aboutsummaryrefslogtreecommitdiffhomepage
path: root/scripts
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-09-18 08:15:25 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-09-18 08:15:25 +0000
commit43ee19f32c3ac89c7312b46f13ebdc50b6896b3b (patch)
tree43172dd588cb89991287ebc7d52d8bd6a8cb229d /scripts
parentc1e3eafa4990b4e1e41d589c0e1a20b641ea1493 (diff)
Now prints an error instead of an anomaly when dynlink fails
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13430 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts')
-rw-r--r--scripts/coqmktop.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 253df86c7..d4a76b6cc 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -237,7 +237,7 @@ let declare_loading_string () =
\n let ppf = Format.std_formatter;;\
\n Mltop.set_top\
\n {Mltop.load_obj=\
-\n (fun f -> if not (Topdirs.load_file ppf f) then failwith \"error\");\
+\n (fun f -> if not (Topdirs.load_file ppf f) then Util.error (\"Could not load plugin \"^f));\
\n Mltop.use_file=Topdirs.dir_use ppf;\
\n Mltop.add_dir=Topdirs.dir_directory;\
\n Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\