aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/stm.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/stm.ml')
-rw-r--r--toplevel/stm.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 19249320b..fc52d3644 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -928,7 +928,7 @@ end = struct (* {{{ *)
let rec manage_slave ~cancel:cancel_user_req id_slave respawn =
let ic, oc, proc =
let rec set_slave_opt = function
- | [] -> ["-async-proofs"; "worker"; string_of_int id_slave]
+ | [] -> ["-async-proofs"; "worker"; string_of_int id_slave; "-feedback-glob"]
| ("-ideslave"|"-emacs"|"-emacs-U")::tl -> set_slave_opt tl
| ("-async-proofs"
|"-compile"