The menu Options has been renamed Tools.

This commit is contained in:
Thibaut Cuvelier 2021-01-28 05:04:39 +01:00
parent 0b56495e48
commit 2720ac5dda

View File

@ -1749,7 +1749,7 @@ bool TextClass::load(string const & path) const
<< to_utf8(makeDisplayPath(layout_file.absFileName()))
<< "'\n(Check `" << name_
<< "')\nCheck your installation and "
"try Options/Reconfigure..."
"try Tools/Reconfigure..."
<< endl;
}