diff options
Diffstat (limited to 'src/main/options')
| -rw-r--r-- | src/main/options | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/main/options b/src/main/options index 35e3df7d2..09b06bd07 100644 --- a/src/main/options +++ b/src/main/options @@ -39,6 +39,9 @@ option fallbackSequential --fallback-sequential bool :default false option incrementalParallel --incremental-parallel bool :default false :link --incremental Use parallel solver even in incremental mode (may print 'unknown's at times) +option interactivePrompt /--no-interactive-prompt bool :default true + turn off interactive prompting while in interactive mode + option segvSpin --segv-spin bool :default false spin on segfault/other crash waiting for gdb undocumented-alias --segv-nospin = --no-segv-spin |