Protection mode Debug On contre Ctrl-D

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8795 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 2 deletions

diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 43807872dc..889e06a8b5 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 ();