diff options
Diffstat (limited to 'toplevel/mltop.ml')
| -rw-r--r-- | toplevel/mltop.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index d9b739354..9b040d70b 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -120,8 +120,8 @@ let ml_load s = with | e when Errors.noncritical e -> let e = Errors.push e in - match e with - | (UserError _ | Failure _ | Not_found as u) -> raise u + match fst e with + | (UserError _ | Failure _ | Not_found as u) -> Exninfo.iraise (u, snd e) | exc -> let msg = report_on_load_obj_error exc in errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++ |