diff options
| author | Emilio Jesus Gallego Arias | 2019-02-04 18:16:39 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-04 18:16:39 +0100 |
| commit | 0439543db9f3be84d59cfdc1dcad34bd114036e3 (patch) | |
| tree | c116ee4f057c34109abfc5fc27a45e57cad436a7 /kernel/dune | |
| parent | c70412ec8b0bb34b7a5607c07d34607a147d834c (diff) | |
[dune] Fix Dune build in Windows.
In order for Dune to work in Windows we need to tweak some script
calls, they need a POSIX shell and the `(run ...)` / `(system ...)`
actions use `cmd.exe` on Windows.
Hopefully, we will rely less on `bash` when Dune can understand Coq
libraries. This affects shell scripts in `kernel/**.sh` for example.
It is interesting to see how faster the Coq Windows build is with Dune
+ Windows.
There are some problems with PATHs that prevent the test suite from
working, these will be fixed in a future PR.
Diffstat (limited to 'kernel/dune')
| -rw-r--r-- | kernel/dune | 4 |
1 files changed, 2 insertions, 2 deletions
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) |