aboutsummaryrefslogtreecommitdiff
path: root/dev/shim
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-03-28 17:18:25 +0100
committerEmilio Jesus Gallego Arias2019-03-28 17:18:25 +0100
commit5408978c2ed5ffb4da885f742cd808bc0b518021 (patch)
tree0fb04cf648a7fc0a81f9d41eeda4a39a11658ccf /dev/shim
parent688e20c432d2639050a62703e1c566ddfbe42b2a (diff)
[dune] Fix shim quoting and add coqc wrapper.
The quoting was incorrect thus scripts didn't properly work.
Diffstat (limited to 'dev/shim')
-rw-r--r--dev/shim/dune18
1 files changed, 15 insertions, 3 deletions
diff --git a/dev/shim/dune b/dev/shim/dune
index 39b4ef492c..e307848292 100644
--- a/dev/shim/dune
+++ b/dev/shim/dune
@@ -7,7 +7,19 @@
(with-outputs-to coqtop-prelude
(progn
(echo "#!/usr/bin/env bash\n")
- (bash "echo \"$(pwd)/%{bin:coqtop} -coqlib $(pwd)/%{project_root}\" \"$@\"")
+ (bash "echo \"$(pwd)/%{bin:coqtop} -coqlib $(pwd)/%{project_root}\" \\$@")
+ (run chmod +x %{targets})))))
+
+(rule
+ (targets coqc-prelude)
+ (deps
+ %{bin:coqc}
+ %{project_root}/theories/Init/Prelude.vo)
+ (action
+ (with-outputs-to coqc-prelude
+ (progn
+ (echo "#!/usr/bin/env bash\n")
+ (bash "echo \"$(pwd)/%{bin:coqc} -coqlib $(pwd)/%{project_root}\" \\$@")
(run chmod +x %{targets})))))
(rule
@@ -20,7 +32,7 @@
(with-outputs-to %{targets}
(progn
(echo "#!/usr/bin/env bash\n")
- (bash "echo \"$(pwd)/%{bin:coqtop.byte} -coqlib $(pwd)/%{project_root}\" \"$@\"")
+ (bash "echo \"$(pwd)/%{bin:coqtop.byte} -coqlib $(pwd)/%{project_root}\" \\$@")
(run chmod +x %{targets})))))
(rule
@@ -36,5 +48,5 @@
(with-outputs-to coqide-prelude
(progn
(echo "#!/usr/bin/env bash\n")
- (bash "echo \"$(pwd)/%{bin:coqide} -coqlib $(pwd)/%{project_root}\" \"$@\"")
+ (bash "echo \"$(pwd)/%{bin:coqide} -coqlib $(pwd)/%{project_root}\" \\$@")
(run chmod +x %{targets})))))