aboutsummaryrefslogtreecommitdiff
path: root/dune
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-02-04 18:16:39 +0100
committerEmilio Jesus Gallego Arias2019-02-04 18:16:39 +0100
commit0439543db9f3be84d59cfdc1dcad34bd114036e3 (patch)
treec116ee4f057c34109abfc5fc27a45e57cad436a7 /dune
parentc70412ec8b0bb34b7a5607c07d34607a147d834c (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 'dune')
-rw-r--r--dune4
1 files changed, 2 insertions, 2 deletions
diff --git a/dune b/dune
index 1706cb44b1..95041512e2 100644
--- a/dune
+++ b/dune
@@ -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