]> matita.cs.unibo.it Git - helm.git/commitdiff
First part of bug #152 (unable to exit from Matita) solved.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 22 Feb 2006 14:00:21 +0000 (14:00 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 22 Feb 2006 14:00:21 +0000 (14:00 +0000)
helm/software/matita/matitaScript.ml

index b8c9505497305dcc0f407d2ae8f448d0c29120e6..d243ebb2ead2ad2c5f65708646cf25c02137e363 100644 (file)
@@ -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