From b41a051cf56a8c32b02df7ce6fe6d6fcd266fd8b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 5 Nov 2018 18:49:45 +0100
Subject: [dune] [coqide] Use copy action instead of (run cp ...)

This is a bit more portable.
---
 ide/dune | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide')

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)
-- 
cgit v1.2.3