aboutsummaryrefslogtreecommitdiff
path: root/dev/shim
diff options
context:
space:
mode:
Diffstat (limited to 'dev/shim')
-rw-r--r--dev/shim/dune13
1 files changed, 13 insertions, 0 deletions
diff --git a/dev/shim/dune b/dev/shim/dune
index 85a0d205da..39b4ef492c 100644
--- a/dev/shim/dune
+++ b/dev/shim/dune
@@ -11,6 +11,19 @@
(run chmod +x %{targets})))))
(rule
+ (targets coqbyte-prelude)
+ (deps
+ %{bin:coqtop.byte}
+ %{lib:coq.kernel:../../stublibs/dllbyterun_stubs.so}
+ %{project_root}/theories/Init/Prelude.vo)
+ (action
+ (with-outputs-to %{targets}
+ (progn
+ (echo "#!/usr/bin/env bash\n")
+ (bash "echo \"$(pwd)/%{bin:coqtop.byte} -coqlib $(pwd)/%{project_root}\" \"$@\"")
+ (run chmod +x %{targets})))))
+
+(rule
(targets coqide-prelude)
(deps
%{bin:coqqueryworker.opt}