aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEnrico Tassi2019-02-11 11:00:40 +0100
committerEnrico Tassi2019-02-11 11:00:40 +0100
commit22bbbd1a8cf5b75e9e9002ce9cfc8b5ced5f355a (patch)
tree0d9d2e99862ab2159719e49963ce05b7f4fa2d5b
parentaa66e4b3e58699db5af904e14247c73744398732 (diff)
[stm] -async-proofs-tac-j accepts only >= 1 (fix #9533)
-rw-r--r--toplevel/coqargs.ml7
1 files changed, 6 insertions, 1 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index b549f22119..1e1a74209f 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -311,8 +311,13 @@ let parse_args ~help ~init arglist : t * string list =
}}
|"-async-proofs-tac-j" ->
+ let j = get_int opt (next ()) in
+ if j <= 0 then begin
+ prerr_endline ("Error: -async-proofs-tac-j only accepts values greater than or equal to 1");
+ exit 1;
+ end;
{ oval with stm_flags = { oval.stm_flags with
- Stm.AsyncOpts.async_proofs_n_tacworkers = (get_int opt (next ()))
+ Stm.AsyncOpts.async_proofs_n_tacworkers = j
}}
|"-async-proofs-worker-priority" ->