diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-08-26 14:58:47 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-08-26 14:58:47 +0200 |
| commit | 9ef5dbb1f340971036aa0c7d4d7a0986188fd971 (patch) | |
| tree | 39a7980164a5127a0ab7e39b5e5c625a1d16daa6 /stm | |
| parent | bbcb802d81fad79fc76bde031bafb130132946ba (diff) | |
Do not pass "-batch" or "-load-vernac-source" to slaves, avoiding errors in
stm test-suite files.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 36689e6e5..5de80bbfc 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -143,9 +143,9 @@ module Make(T : Task) = struct | [] -> !Flags.async_proofs_flags_for_workers @ ["-toploop"; T.name^"top"; "-worker-id"; id] - | ("-ideslave"|"-emacs"|"-emacs-U")::tl -> set_slave_opt tl + | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl | ("-async-proofs" |"-toploop" |"-vi2vo" |"-compile" - |"-compile-verbose")::_::tl -> set_slave_opt tl + | "-load-vernac-source" | "-compile-verbose")::_::tl -> set_slave_opt tl | x::tl -> x :: set_slave_opt tl in let args = Array.of_list (set_slave_opt (List.tl (Array.to_list Sys.argv))) in |