diff options
Diffstat (limited to 'dune')
| -rw-r--r-- | dune | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -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 |