aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorThéo Zimmermann2019-02-05 09:49:54 +0100
committerThéo Zimmermann2019-02-05 09:49:54 +0100
commit740ec848acc0b127fad7ba5b703bc00364126c71 (patch)
treed72ced5aaa9d4b4ba3061e649a0e9462f238b5a0 /tools
parent5c1d7fc460d0b98a1dfbcf151079dbacb64c9330 (diff)
parent0439543db9f3be84d59cfdc1dcad34bd114036e3 (diff)
Merge PR #8421: [dune] Fix Dune build in Windows.
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: gares Ack-by: maximedenes Ack-by: ppedrot
Diffstat (limited to 'tools')
-rw-r--r--tools/coq_dune.ml9
1 files changed, 7 insertions, 2 deletions
diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml
index 6681b79e38..68371edcb1 100644
--- a/tools/coq_dune.ml
+++ b/tools/coq_dune.ml
@@ -271,8 +271,13 @@ let exec_ifile f =
match Array.length Sys.argv with
| 1 -> f stdin
| 2 ->
- let ic = open_in Sys.argv.(1) in
- (try f ic with _ -> close_in ic)
+ let in_file = Sys.argv.(1) in
+ begin try
+ let ic = open_in in_file in
+ (try f ic
+ with _ -> eprintf "Error: exec_ifile@\n%!"; close_in ic)
+ with _ -> eprintf "Error: cannot open input file %s@\n%!" in_file
+ end
| _ -> eprintf "Error: wrong number of arguments@\n%!"; exit 1
let _ =