diff options
| author | Hugo Herbelin | 2014-07-01 10:39:52 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-07-01 11:55:03 +0200 |
| commit | d755f77f9cc4760c403e588aea085733cd1f2979 (patch) | |
| tree | 321c78644e5758231848fb0505655f96a18eb0dd | |
| parent | 6987d434687890b6218b252b89b55ab5d3ef2221 (diff) | |
More informative message when Mltop.load_object fails.
| -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 695fd3b82e..3c7bd8e24e 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 = |