From f8b2de715c57d3d66fff38b41fa3b4351c015c11 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?S=C3=A9bastien=20Villemot?= <sebastien@dynare.org>
Date: Mon, 18 Dec 2023 16:24:22 +0100
Subject: [PATCH] Drop unused options_.minimal_workspace
---
src/ModFile.cc | 3 ---
1 file changed, 3 deletions(-)
diff --git a/src/ModFile.cc b/src/ModFile.cc
index 1a259fe5..1df12611 100644
--- a/src/ModFile.cc
+++ b/src/ModFile.cc
@@ -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)
--
GitLab