summaryrefslogtreecommitdiff
path: root/cparser/Cerrors.ml
diff options
context:
space:
mode:
Diffstat (limited to 'cparser/Cerrors.ml')
-rw-r--r--cparser/Cerrors.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/cparser/Cerrors.ml b/cparser/Cerrors.ml
index 83cd019..23ec171 100644
--- a/cparser/Cerrors.ml
+++ b/cparser/Cerrors.ml
@@ -41,6 +41,9 @@ let warning fmt =
incr num_warnings;
eprintf ("@[<hov 2>" ^^ fmt ^^ ".@]@.")
+let info fmt =
+ eprintf ("@[<hov 2>" ^^ fmt ^^ ".@]@.")
+
let check_errors () =
if !num_errors > 0 then
eprintf "@[<hov 0>%d error%s detected.@]@."