diff options
Diffstat (limited to 'src/reporting_basic.ml')
| -rw-r--r-- | src/reporting_basic.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/reporting_basic.ml b/src/reporting_basic.ml index 5ff43208..69c5c084 100644 --- a/src/reporting_basic.ml +++ b/src/reporting_basic.ml @@ -220,5 +220,6 @@ let report_error e = let (m1, verb_pos, pos_l, m2) = dest_err e in (print_err_internal verb_pos false pos_l m1 m2; exit 1) - - +let print_error e = + let (m1, verb_pos, pos_l, m2) = dest_err e in + print_err_internal verb_pos false pos_l m1 m2 |