aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--Makefile.build4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build
index 5894c133b..16e7cdaa4 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -366,12 +366,12 @@ else
bin/coq-interface$(EXE):
echo "#!/bin/sh" > $@
- echo "exec coqtop -require CoqInterface" >> $@
+ echo 'exec '$(BINDIR)'/coqtop -require CoqInterface' >> $@
chmod +x $@
bin/coq-parser$(EXE):
echo "#!/bin/sh" > $@
- echo "exec coqtop -batch -l CoqParser" >> $@
+ echo 'exec '$(BINDIR)'/coqtop -batch -l CoqParser' >> $@
chmod +x $@
endif # of HASNATDYNLINK