From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 21 Nov 2006 21:38:49 +0000
Subject: Imported Upstream version 8.1~gamma

---
 toplevel/vernac.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'toplevel/vernac.ml')

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index afe72f0f..710b814d 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: vernac.ml 8924 2006-06-08 17:49:01Z notin $ *)
+(* $Id: vernac.ml 9133 2006-09-12 14:52:07Z notin $ *)
 
 (* Parsing of vernacular. *)
 
@@ -162,12 +162,12 @@ let rec vernac_com interpfun (loc,com) =
     | v -> if not !just_parsing then interpfun v
 
   in 
-  try
-    if do_translate () then pr_new_syntax loc (Some com);
-    interp com
-  with e -> 
-    Format.set_formatter_out_channel stdout;
-    raise (DuringCommandInterp (loc, e))
+    try
+      if do_translate () then pr_new_syntax loc (Some com);
+      interp com
+    with e -> 
+      Format.set_formatter_out_channel stdout;
+      raise (DuringCommandInterp (loc, e))
 
 and vernac interpfun input =
   vernac_com interpfun (parse_phrase input)
-- 
cgit v1.2.3