Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

1 files changed, 3 insertions, 2 deletions

diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 43807872..889e06a8 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -76,11 +76,12 @@ let rec prompt level =
   begin
     msg (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ");
     flush stdout;
-    let inst = read_line () in
+    let exit () = skip:=0;allskip:=0;raise Sys.Break in
+    let inst = try read_line () with End_of_file -> exit () in
     match inst with
     | ""  -> true
     | "s" -> false
-    | "x" -> print_char (Char.chr 8);skip:=0;allskip:=0;raise Sys.Break
+    | "x" -> print_char (Char.chr 8); exit ()
     | "h"| "?" ->
       begin
         help ();