summaryrefslogtreecommitdiff
path: root/src/main
diff options
context:
space:
mode:
Diffstat (limited to 'src/main')
-rw-r--r--src/main/options3
1 files changed, 1 insertions, 2 deletions
diff --git a/src/main/options b/src/main/options
index 6defc8642..47e397d11 100644
--- a/src/main/options
+++ b/src/main/options
@@ -30,8 +30,7 @@ option threadArgv std::vector<std::string>
option thread_id int :default -1
Thread ID, for internal use in case of multi-threaded run
option separateOutput bool :default false
- In multi-threaded setting print output of each thread at the
- end of run, separated by a divider ("----").
+ In multi-threaded setting print output of each thread at the end of run, separated by a divider ("----").
option sharingFilterByLength --filter-lemma-length=N int :default -1 :read-write
don't share lemmas strictly longer than N
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback