summaryrefslogtreecommitdiff
path: root/src/options/options.h
diff options
context:
space:
mode:
authorMathias Preiner <mathias.preiner@gmail.com>2019-08-14 13:12:19 -0700
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2019-08-14 15:12:19 -0500
commit044891b406eb3ee143403ad8fecd7acb99d17ecb (patch)
treef90d35b378da21c2fe889149eb974709292af609 /src/options/options.h
parent29639a7df6ddf105803431cc85888c9416af6af6 (diff)
Remove option --continued-execution. (#3189)
Diffstat (limited to 'src/options/options.h')
-rw-r--r--src/options/options.h1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/options/options.h b/src/options/options.h
index 020350c49..0d26c60b9 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -198,7 +198,6 @@ public:
InstFormatMode getInstFormatMode() const;
OutputLanguage getOutputLanguage() const;
bool getCheckProofs() const;
- bool getContinuedExecution() const;
bool getDumpInstantiations() const;
bool getDumpModels() const;
bool getDumpProofs() const;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback