aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorgareuselesinge2013-10-03 09:09:24 +0000
committergareuselesinge2013-10-03 09:09:24 +0000
commitf626b7a90c641ac3fb40d8acf37a8985df2480a9 (patch)
tree23797d18d83341af3b25e07ee51517da2a750fc8 /lib
parentad513f2343d3cced4050b95803b33b28dd2382f8 (diff)
STM: number of slaves passed by the command line
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16839 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
-rw-r--r--lib/flags.ml1
-rw-r--r--lib/flags.mli1
2 files changed, 2 insertions, 0 deletions
diff --git a/lib/flags.ml b/lib/flags.ml
index 9f4e81408e..ec6469affe 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -47,6 +47,7 @@ let batch_mode = ref false
let ide_slave_mode = ref false
let coq_slave_mode = ref (-1)
+let coq_slaves_number = ref 1
let debug = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index a5abca7a9f..5774f3ad41 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -14,6 +14,7 @@ val batch_mode : bool ref
val ide_slave_mode : bool ref
val coq_slave_mode : int ref
+val coq_slaves_number : int ref
val debug : bool ref