]> matita.cs.unibo.it Git - helm.git/commitdiff
a parser error is now logged as an error!
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 15 Jun 2005 15:43:06 +0000 (15:43 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 15 Jun 2005 15:43:06 +0000 (15:43 +0000)
helm/matita/matitac.ml

index d9300218375851113a45f246c6f4c467e2acfb07..e7cdef9f4afb898ac82d492b58dab4a03a108965 100644 (file)
@@ -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 ->