aboutsummaryrefslogtreecommitdiff
path: root/topbin
diff options
context:
space:
mode:
Diffstat (limited to 'topbin')
-rw-r--r--topbin/coqtop_byte_bin.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/topbin/coqtop_byte_bin.ml b/topbin/coqtop_byte_bin.ml
index 604c6e251a..7e977ca0f2 100644
--- a/topbin/coqtop_byte_bin.ml
+++ b/topbin/coqtop_byte_bin.ml
@@ -11,9 +11,9 @@
(* We register this handler for lower-level toplevel loading code *)
let _ = CErrors.register_handler (function
| Symtable.Error e ->
- Pp.str (Format.asprintf "%a" Symtable.report_error e)
+ Some (Pp.str (Format.asprintf "%a" Symtable.report_error e))
| _ ->
- raise CErrors.Unhandled
+ None
)
let drop_setup () =