diff options
| -rw-r--r-- | toplevel/mltop.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 695fd3b82..3c7bd8e24 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -131,7 +131,9 @@ let dir_ml_load s = try Dynlink.loadfile gname; with Dynlink.Error a -> - errorlabstrm "Mltop.load_object" (str (Dynlink.error_message a)) + errorlabstrm "Mltop.load_object" + (strbrk "while loading " ++ str s ++ + strbrk ": " ++ str (Dynlink.error_message a)) (* Dynamic interpretation of .ml *) let dir_ml_use s = |