Drop unused options_.minimal_workspace

master
Sébastien Villemot 2023-12-18 16:24:22 +01:00
parent 638c49d96e
commit f8b2de715c
No known key found for this signature in database
GPG Key ID: 2CECE9350ECEBE4A
1 changed files with 0 additions and 3 deletions

View File

@ -918,9 +918,6 @@ ModFile::writeMOutput(const string& basename, bool clear_all, bool clear_global,
config.writeHooks(mOutputFile);
mOutputFile << "global_initialization;" << endl;
if (minimal_workspace)
mOutputFile << "options_.minimal_workspace = true;" << endl;
if (console)
mOutputFile << "options_.console_mode = true;" << endl << "options_.nodisplay = true;" << endl;
if (nograph)