diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-07-01 10:39:52 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-07-01 11:55:03 +0200 |
| commit | d755f77f9cc4760c403e588aea085733cd1f2979 (patch) | |
| tree | 321c78644e5758231848fb0505655f96a18eb0dd /toplevel/mltop.ml | |
| parent | 6987d434687890b6218b252b89b55ab5d3ef2221 (diff) | |
More informative message when Mltop.load_object fails.
Diffstat (limited to 'toplevel/mltop.ml')
| -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 = |