diff options
| author | Gaëtan Gilbert | 2020-11-30 16:40:37 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-11-30 16:40:37 +0100 |
| commit | 81bc69df73d20c5c4d0e1ccc77255c0c6c118abc (patch) | |
| tree | 06ce0274e01d4691c41bf04f3fe6f3a49c1f78b0 /dev/shim | |
| parent | 0af89e4c04b1ecf437a86b50a34a17eddee56b76 (diff) | |
dune: Don't echo "$(pwd)" when creating the shims
AFAICT `echo "$(pwd)"` is unsound for the dune cache when called from
different paths (typically different git worktrees).
Diffstat (limited to 'dev/shim')
| -rw-r--r-- | dev/shim/dune | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/dev/shim/dune b/dev/shim/dune index 84b2e642e8..8006c629ed 100644 --- a/dev/shim/dune +++ b/dev/shim/dune @@ -7,7 +7,7 @@ (with-stdout-to coqtop-prelude (progn (echo "#!/usr/bin/env bash\n") - (bash "echo \"$(pwd)/%{bin:coqtop} -coqlib $(pwd)/%{project_root}\" \\$@") + (bash "echo '$(dirname $0)/%{bin:coqtop} -coqlib $(dirname $0)/%{project_root}' \\$@") (run chmod +x %{targets}))))) (rule @@ -19,7 +19,7 @@ (with-stdout-to coqc-prelude (progn (echo "#!/usr/bin/env bash\n") - (bash "echo \"$(pwd)/%{bin:coqc} -coqlib $(pwd)/%{project_root}\" \\$@") + (bash "echo '$(dirname $0)/%{bin:coqc} -coqlib $(dirname $0)/%{project_root}' \\$@") (run chmod +x %{targets}))))) (rule @@ -32,7 +32,7 @@ (with-stdout-to %{targets} (progn (echo "#!/usr/bin/env bash\n") - (bash "echo \"$(pwd)/%{bin:coqtop.byte} -coqlib $(pwd)/%{project_root}\" \\$@") + (bash "echo '$(dirname $0)/%{bin:coqtop.byte} -coqlib $(dirname $0)/%{project_root}' \\$@") (run chmod +x %{targets}))))) (rule @@ -48,5 +48,5 @@ (with-stdout-to coqide-prelude (progn (echo "#!/usr/bin/env bash\n") - (bash "echo \"$(pwd)/%{bin:coqide} -coqlib $(pwd)/%{project_root}\" \\$@") + (bash "echo '$(dirname $0)/%{bin:coqide} -coqlib $(dirname $0)/%{project_root}' \\$@") (run chmod +x %{targets}))))) |