diff options
| author | Enrico Tassi | 2019-02-11 11:00:40 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-02-11 11:00:40 +0100 |
| commit | 22bbbd1a8cf5b75e9e9002ce9cfc8b5ced5f355a (patch) | |
| tree | 0d9d2e99862ab2159719e49963ce05b7f4fa2d5b /toplevel | |
| parent | aa66e4b3e58699db5af904e14247c73744398732 (diff) | |
[stm] -async-proofs-tac-j accepts only >= 1 (fix #9533)
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqargs.ml | 7 |
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" -> |
