From 43ee19f32c3ac89c7312b46f13ebdc50b6896b3b Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 18 Sep 2010 08:15:25 +0000 Subject: 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 --- scripts/coqmktop.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'scripts') 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) };;\ -- cgit v1.2.3