summaryrefslogtreecommitdiff
path: root/src/main/options
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2014-04-04 14:49:17 -0400
committerMorgan Deters <mdeters@cs.nyu.edu>2014-04-04 15:27:16 -0400
commit00d068f91c675edbe63c2f8c1dae283f300dd4cc (patch)
tree32a8233569ffc5f2218c43d1852a7aa7568766c6 /src/main/options
parent9e2e46bf9c81e9a5a46262904a26689cfa67c308 (diff)
Allow turning off the interactive prompt while in interactive mode.
Diffstat (limited to 'src/main/options')
-rw-r--r--src/main/options3
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback