From 32c96a65487f71bb22a609c18eac315bd700dc36 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 22 Feb 2006 14:00:21 +0000 Subject: [PATCH] First part of bug #152 (unable to exit from Matita) solved. --- matita/matitaScript.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml index b8c950549..d243ebb2e 100644 --- a/matita/matitaScript.ml +++ b/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 -- 2.39.2