diff --git a/src/tools/unix_scheduler.ml b/src/tools/unix_scheduler.ml
index a190586de7271cf74dfd8bf69f9e8c38e9977993..c541e115bf6dd22306a97981add87343cb4e2d59 100644
--- a/src/tools/unix_scheduler.ml
+++ b/src/tools/unix_scheduler.ml
@@ -45,18 +45,22 @@ module Unix_scheduler = struct
 
      let prompt_delay = ref 0
      let print_prompt = ref true
-     let prompt = ref "> "
+     let prompt_string = ref "> "
 
      (* [main_loop interp] starts the scheduler. On idle, standard input is
         read.  When a complete line is read from stdin, it is passed
         as a string to the function [interp] *)
-     let main_loop interp =
+     let main_loop ?prompt interp =
+       begin match prompt with
+       | None -> ()
+       | Some s -> prompt_string := s
+       end;
        try
          while true do
            if !print_prompt then begin
              prompt_delay := !prompt_delay + 1;
-             if !prompt_delay = 1 then begin
-               Format.printf "%s@?" !prompt;
+             if !prompt_string <> "" && !prompt_delay = 1 then begin
+               Format.printf "%s@?" !prompt_string;
                prompt_delay := 0;
                print_prompt := false;
              end
@@ -87,7 +91,8 @@ module Unix_scheduler = struct
                    | (_,t,_) :: _ -> t -. time
                    (* or the time left until the next timeout otherwise *)
                  in
-                 let a,_,_ = Unix.select [Unix.stdin] [] [] delay in
+                 let a,_,_ = Unix.select
+                               (if !prompt_string <> "" then [Unix.stdin] else []) [] [] delay in
                  match a with
                  | [_] ->
                     let n = Unix.read Unix.stdin buf 0 256 in
diff --git a/src/tools/unix_scheduler.mli b/src/tools/unix_scheduler.mli
index e2aab92065ce27b80449e60836dca279af78c9d5..fe9f72b221bbee1836bc7d2d7aa7c1d9b801b7f2 100644
--- a/src/tools/unix_scheduler.mli
+++ b/src/tools/unix_scheduler.mli
@@ -15,6 +15,6 @@ module Unix_scheduler : sig
     registered at the same time. Functions registered with higher
     priority will be called first. *)
 
-    val main_loop: (string -> 'a) -> unit
+    val main_loop: ?prompt:string -> (string -> 'a) -> unit
 
 end
diff --git a/src/tools/why3replay.ml b/src/tools/why3replay.ml
index 4addef669c4b95ef1665c1429a2f22da01597c36..36ba65faf956f8d8ef9171b1e6493a7f0248078d 100644
--- a/src/tools/why3replay.ml
+++ b/src/tools/why3replay.ml
@@ -391,7 +391,7 @@ let () =
     if found_obs then eprintf "[Warning] session is obsolete@.";
     if some_merge_miss then eprintf "[Warning] some goals were missed during merge@.";
     add_to_check_no_smoke some_merge_miss found_obs cont;
-    Unix_scheduler.Unix_scheduler.main_loop (fun _ -> ());
+    Unix_scheduler.Unix_scheduler.main_loop ~prompt:"" (fun _ -> ());
     eprintf "main replayer loop exited unexpectedly@.";
     exit 1
   with