aboutsummaryrefslogtreecommitdiff
path: root/scripts
diff options
context:
space:
mode:
Diffstat (limited to 'scripts')
-rw-r--r--scripts/coqmktop.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 441926becf..0373b82e94 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -233,8 +233,7 @@ let declare_loading_string () =
(* create a temporary main file to link *)
let create_tmp_main_file modules =
- let main_name = Filename.temp_file "coqmain" ".ml" in
- let oc = open_out main_name in
+ let main_name,oc = Filename.open_temp_file "coqmain" ".ml" in
try
(* Add the pre-linked modules *)
output_string oc "List.iter Mltop.add_known_module [\"";