aboutsummaryrefslogtreecommitdiffhomepage
path: root/scripts
diff options
context:
space:
mode:
authorGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-03-20 19:15:47 +0000
committerGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-03-20 19:15:47 +0000
commita0d3c8c3268f23c3fed89f9c30df9c3bbd604034 (patch)
tree9ee5c45e53a1d38571825a7cfcae33d4f18ba23f /scripts
parenteb04887fe4d48deabc029e067a8d0e4515879e8a (diff)
replaced dir_load by load_file because dir_load does not raise an exception when loading fails
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12000 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts')
-rw-r--r--scripts/coqmktop.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 85ea683e9..2c9c6d213 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -236,7 +236,8 @@ let declare_loading_string () =
let ppf = Format.std_formatter;;
Mltop.set_top
- {Mltop.load_obj=Topdirs.dir_load ppf;
+ {Mltop.load_obj=
+ (fun f -> if not (Topdirs.load_file ppf f) then failwith \"error\");
Mltop.use_file=Topdirs.dir_use ppf;
Mltop.add_dir=Topdirs.dir_directory;
Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\n"