summaryrefslogtreecommitdiff
path: root/scripts
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2013-05-08 17:47:10 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2013-05-08 17:47:10 +0200
commit499a11a45b5711d4eaabe84a80f0ad3ae539d500 (patch)
tree09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /scripts
parentbf12eb93f3f6a6a824a10878878fadd59745aae0 (diff)
Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg
Diffstat (limited to 'scripts')
-rw-r--r--scripts/coqmktop.ml13
1 files changed, 6 insertions, 7 deletions
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 5bc77457..b75984e3 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -45,8 +45,7 @@ let camlp4topobjs =
[ "Camlp4Top.cmo";
"Camlp4Parsers/Camlp4OCamlRevisedParser.cmo";
"Camlp4Parsers/Camlp4OCamlParser.cmo";
- "Camlp4Parsers/Camlp4GrammarParser.cmo";
- "q_util.cmo"; "q_coqast.cmo" ]
+ "Camlp4Parsers/Camlp4GrammarParser.cmo" ]
let topobjs = camlp4topobjs
let gramobjs = []
@@ -257,8 +256,8 @@ let create_tmp_main_file modules =
output_string oc "Coqtop.start();;\n";
close_out oc;
main_name
- with e ->
- clean main_name; raise e
+ with reraise ->
+ clean main_name; raise reraise
(* main part *)
let main () =
@@ -311,10 +310,10 @@ let main () =
clean main_file;
(* command gives the exit code in HSB, and signal in LSB !!! *)
if retcode > 255 then retcode lsr 8 else retcode
- with e ->
- clean main_file; raise e
+ with reraise ->
+ clean main_file; raise reraise
let retcode =
- try Printexc.print main () with _ -> 1
+ try Printexc.print main () with any -> 1
let _ = exit retcode