From d5b987466c6c1642175fed2ad49c45531f237aa2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 5 May 2006 18:17:32 +0000
Subject: 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
---
 proofs/tactic_debug.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'proofs')

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 ();
-- 
cgit v1.2.3