From eb52433fbf064ae7c6f76178fb142a5e7b9e2dd1 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Sat, 2 Jun 2012 15:27:20 +0000
Subject: Fixed printing error problem... A line had disappeared in a previous
 patch.

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

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a486de2e2e..779cd06bf3 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -351,6 +351,8 @@ let init arglist =
       flush_all();
       if not !batch_mode then
         fatal_error (str "Error during initialization:" ++ fnl () ++ Toplevel.print_toplevel_error e)
+      else
+        fatal_error (Toplevel.print_toplevel_error e)
   end;
   if !batch_mode then
     (flush_all();
-- 
cgit v1.2.3