diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-08-14 13:12:19 -0700 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-14 15:12:19 -0500 |
| commit | 044891b406eb3ee143403ad8fecd7acb99d17ecb (patch) | |
| tree | f90d35b378da21c2fe889149eb974709292af609 /src/options | |
| parent | 29639a7df6ddf105803431cc85888c9416af6af6 (diff) | |
Remove option --continued-execution. (#3189)
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/didyoumean_test.cpp | 1 | ||||
| -rw-r--r-- | src/options/main_options.toml | 10 | ||||
| -rw-r--r-- | src/options/options.h | 1 | ||||
| -rw-r--r-- | src/options/options_public_functions.cpp | 4 |
4 files changed, 0 insertions, 16 deletions
diff --git a/src/options/didyoumean_test.cpp b/src/options/didyoumean_test.cpp index 7230f544d..c6d92c97b 100644 --- a/src/options/didyoumean_test.cpp +++ b/src/options/didyoumean_test.cpp @@ -734,7 +734,6 @@ set<string> getOptionStrings() { "incremental-parallel", "no-incremental-parallel", "no-interactive-prompt", - "continued-execution", "immediate-exit", "segv-spin", "no-segv-spin", diff --git a/src/options/main_options.toml b/src/options/main_options.toml index 9f75e9426..71c964678 100644 --- a/src/options/main_options.toml +++ b/src/options/main_options.toml @@ -163,16 +163,6 @@ header = "options/main_options.h" help = "interactive prompting while in interactive mode" [[option]] - name = "continuedExecution" - category = "regular" - long = "continued-execution" - type = "bool" - default = "false" - links = ["--interactive", "--no-interactive-prompt"] - read_only = true - help = "continue executing commands, even on error" - -[[option]] name = "segvSpin" category = "regular" long = "segv-spin" 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; diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp index 39f2eb140..43b44b93e 100644 --- a/src/options/options_public_functions.cpp +++ b/src/options/options_public_functions.cpp @@ -54,10 +54,6 @@ bool Options::getCheckProofs() const{ return (*this)[options::checkProofs]; } -bool Options::getContinuedExecution() const{ - return (*this)[options::continuedExecution]; -} - bool Options::getDumpInstantiations() const{ return (*this)[options::dumpInstantiations]; } |