From 48eb0079ac853b5527f2629838ef307231c07ee2 Mon Sep 17 00:00:00 2001
From: bertot
Date: Sat, 10 Feb 2001 08:48:20 +0000
Subject: All errors were not well reported before.  In particular syntax
 errors were not correctly encapsulated in an acknowledge message.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1368 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/protectedtoplevel.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/toplevel/protectedtoplevel.ml b/toplevel/protectedtoplevel.ml
index 322a28fa1b..26ca3b1cc2 100644
--- a/toplevel/protectedtoplevel.ml
+++ b/toplevel/protectedtoplevel.ml
@@ -127,7 +127,10 @@ let rec parse_one_command_group input_channel =
 				  output_results_nl
 				    (acknowledge_command
 				       !global_request_id rank (Some e1))
-			      | e -> raise e));
+			      | e -> 
+				  output_results_nl
+				    (acknowledge_command
+				       !global_request_id rank (Some e))));
 		    rearm_break();
 		    flush_until_end_of_stream stream_tail
 	      	end
-- 
cgit v1.2.3