From: Claudio Sacerdoti Coen Date: Wed, 15 Jun 2005 15:43:06 +0000 (+0000) Subject: a parser error is now logged as an error! X-Git-Tag: INDEXING_NO_PROOFS~144 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2d09c6299ae9601499228665a89da065ecd390ae;p=helm.git a parser error is now logged as an error! --- diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml index d93002183..e7cdef9f4 100644 --- a/helm/matita/matitac.ml +++ b/helm/matita/matitac.ml @@ -76,7 +76,7 @@ let run_script fname = with | CicTextualParser2.Parse_error (floc,err) -> let (x, y) = CicAst.loc_of_floc floc in - MatitaLog.message (sprintf "Parse error at %d-%d: %s" x y err); + MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err); Http_getter.sync_dump_file (); exit 1 | exn ->