diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-18 08:15:25 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-18 08:15:25 +0000 |
| commit | 43ee19f32c3ac89c7312b46f13ebdc50b6896b3b (patch) | |
| tree | 43172dd588cb89991287ebc7d52d8bd6a8cb229d /scripts | |
| parent | c1e3eafa4990b4e1e41d589c0e1a20b641ea1493 (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.ml | 2 |
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) };;\ |