aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-11-05 18:49:45 +0100
committerEmilio Jesus Gallego Arias2018-11-06 10:35:48 +0100
commitb41a051cf56a8c32b02df7ce6fe6d6fcd266fd8b (patch)
treef49b5a6e223d9073bd9da053d0f20245ab52b193
parentefe60d3c1b09bc059053b7383e068ddc05248dac (diff)
[dune] [coqide] Use copy action instead of (run cp ...)
This is a bit more portable.
-rw-r--r--ide/dune2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/dune b/ide/dune
index 5714b1370e..aeb5424aff 100644
--- a/ide/dune
+++ b/ide/dune
@@ -35,7 +35,7 @@
(rule
(targets coqide_os_specific.ml)
(deps (:in-file coqide_X11.ml.in)) ; TODO support others
- (action (run cp %{in-file} %{targets})))
+ (action (copy# %{in-file} %{targets})))
(executable
(name coqide_main)