aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-07-23 00:40:51 +0200
committerEmilio Jesus Gallego Arias2019-07-23 00:40:51 +0200
commitae82afbaebb7f3a328498d4cc541d299423a7637 (patch)
tree57f6b25e70e38ef7e92dce6fa4025e1466910744 /dev
parent7cdab2e35f21c5bbd4f98fcb49c7b7bd24419849 (diff)
parent9b929e16b1123674c737c1cef2002f5a3c3f2d39 (diff)
Merge PR #10541: Dune: fix build_all_stdlib rule
Ack-by: ejgallego
Diffstat (limited to 'dev')
-rw-r--r--dev/shim/dune8
1 files changed, 4 insertions, 4 deletions
diff --git a/dev/shim/dune b/dev/shim/dune
index e307848292..84b2e642e8 100644
--- a/dev/shim/dune
+++ b/dev/shim/dune
@@ -4,7 +4,7 @@
%{bin:coqtop}
%{project_root}/theories/Init/Prelude.vo)
(action
- (with-outputs-to coqtop-prelude
+ (with-stdout-to coqtop-prelude
(progn
(echo "#!/usr/bin/env bash\n")
(bash "echo \"$(pwd)/%{bin:coqtop} -coqlib $(pwd)/%{project_root}\" \\$@")
@@ -16,7 +16,7 @@
%{bin:coqc}
%{project_root}/theories/Init/Prelude.vo)
(action
- (with-outputs-to coqc-prelude
+ (with-stdout-to coqc-prelude
(progn
(echo "#!/usr/bin/env bash\n")
(bash "echo \"$(pwd)/%{bin:coqc} -coqlib $(pwd)/%{project_root}\" \\$@")
@@ -29,7 +29,7 @@
%{lib:coq.kernel:../../stublibs/dllbyterun_stubs.so}
%{project_root}/theories/Init/Prelude.vo)
(action
- (with-outputs-to %{targets}
+ (with-stdout-to %{targets}
(progn
(echo "#!/usr/bin/env bash\n")
(bash "echo \"$(pwd)/%{bin:coqtop.byte} -coqlib $(pwd)/%{project_root}\" \\$@")
@@ -45,7 +45,7 @@
%{project_root}/coqide-server.install
%{project_root}/coqide.install)
(action
- (with-outputs-to coqide-prelude
+ (with-stdout-to coqide-prelude
(progn
(echo "#!/usr/bin/env bash\n")
(bash "echo \"$(pwd)/%{bin:coqide} -coqlib $(pwd)/%{project_root}\" \\$@")