Merge PR #8421: [dune] Fix Dune build in Windows.

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: gares
Ack-by: maximedenes
Ack-by: ppedrot

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