diff options
| author | Théo Zimmermann | 2019-02-05 09:49:54 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-02-05 09:49:54 +0100 |
| commit | 740ec848acc0b127fad7ba5b703bc00364126c71 (patch) | |
| tree | d72ced5aaa9d4b4ba3061e649a0e9462f238b5a0 | |
| parent | 5c1d7fc460d0b98a1dfbcf151079dbacb64c9330 (diff) | |
| parent | 0439543db9f3be84d59cfdc1dcad34bd114036e3 (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
| -rw-r--r-- | Makefile.dune | 2 | ||||
| -rw-r--r-- | dune | 4 | ||||
| -rw-r--r-- | kernel/byterun/dune | 4 | ||||
| -rw-r--r-- | kernel/dune | 4 | ||||
| -rw-r--r-- | test-suite/misc/universes/dune | 2 | ||||
| -rw-r--r-- | tools/coq_dune.ml | 9 |
6 files changed, 15 insertions, 10 deletions
diff --git a/Makefile.dune b/Makefile.dune index ee3e2d6cb7..78ecc4b056 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -40,7 +40,7 @@ help: voboot: dune build $(DUNEOPT) @vodeps - dune exec coq_dune $(BUILD_CONTEXT)/.vfiles.d + dune exec ./tools/coq_dune.exe $(BUILD_CONTEXT)/.vfiles.d states: voboot dune build $(DUNEOPT) theories/Init/Prelude.vo @@ -19,7 +19,7 @@ (deps (source_tree theories) (source_tree plugins)) - (action (with-stdout-to .vfiles.d (system "%{bin:coqdep} -dyndep opt -noglob -boot `find theories plugins -type f -name *.v`")))) + (action (with-stdout-to .vfiles.d (bash "%{bin:coqdep} -dyndep opt -noglob -boot `find theories plugins -type f -name *.v`")))) (alias (name vodeps) @@ -35,7 +35,7 @@ (rule (targets revision) (deps (:rev-script dev/tools/make_git_revision.sh)) - (action (with-stdout-to revision (run %{rev-script})))) + (action (with-stdout-to revision (bash %{rev-script})))) ; Use summary.log as the target (alias diff --git a/kernel/byterun/dune b/kernel/byterun/dune index 3a714a8a59..c3c44670be 100644 --- a/kernel/byterun/dune +++ b/kernel/byterun/dune @@ -6,5 +6,5 @@ (rule (targets coq_jumptbl.h) - (deps (:h-file coq_instruct.h)) - (action (run ./make_jumptbl.sh %{h-file} %{targets}))) + (deps (:h-file coq_instruct.h) make_jumptbl.sh) + (action (bash "./make_jumptbl.sh %{h-file} %{targets}"))) diff --git a/kernel/dune b/kernel/dune index 79161519ba..1f2d696a36 100644 --- a/kernel/dune +++ b/kernel/dune @@ -8,8 +8,8 @@ (rule (targets copcodes.ml) - (deps (:h-file byterun/coq_instruct.h) make-opcodes) - (action (run ./make_opcodes.sh %{h-file} %{targets}))) + (deps (:h-file byterun/coq_instruct.h) make-opcodes make_opcodes.sh) + (action (bash "./make_opcodes.sh %{h-file} %{targets}"))) (executable (name write_uint63) diff --git a/test-suite/misc/universes/dune b/test-suite/misc/universes/dune index 58bba300d2..0772f95604 100644 --- a/test-suite/misc/universes/dune +++ b/test-suite/misc/universes/dune @@ -5,4 +5,4 @@ (source_tree ../../../plugins)) (action (with-outputs-to all_stdlib.v - (run ./build_all_stdlib.sh)))) + (bash "./build_all_stdlib.sh")))) 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 _ = |