From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 22 Feb 2006 14:00:21 +0000 (+0000)
Subject: First part of bug #152 (unable to exit from Matita) solved.
X-Git-Tag: make_still_working~7541
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b8d37cdd7541fb898f814e5ca3e6ca0137a5db44;p=helm.git

First part of bug #152 (unable to exit from Matita) solved.
---

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index b8c950549..d243ebb2e 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -803,6 +803,7 @@ object (self)
     try
       is_there_only_comments self#lexicon_status s
     with 
+    | HExtlib.Localized _
     | CicNotationParser.Parse_error _ -> false
     | Margin | End_of_file -> true