aboutsummaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-11-25 15:14:15 +0100
committerGitHub2018-11-25 15:14:15 +0100
commit550472c67198353120cdc02b42683024b5b39765 (patch)
treecf1978d1778ef454d94bc8cf1c75f3954d3058e1 /tests
parentb8c4bf77c19670099b1fea44f3ab6204faa25d6b (diff)
parent09b917593e90233d7a55610e9ce7886de77ef576 (diff)
Merge pull request coq/ltac2#88 from wilcoxjay/tests-detect-coqbin
Autodetect COQBIN in tests/Makefile
Diffstat (limited to 'tests')
-rw-r--r--tests/Makefile4
1 files changed, 4 insertions, 0 deletions
diff --git a/tests/Makefile b/tests/Makefile
index 9370b063f8..37915e0d6f 100644
--- a/tests/Makefile
+++ b/tests/Makefile
@@ -1,3 +1,7 @@
+ifeq "$(COQBIN)" ""
+ COQBIN=$(dir $(shell which coqtop))/
+endif
+
all: $(patsubst %.v,%.v.log,$(wildcard *.v))
%.v.log: %.v