aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/Makefile
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-07-19 12:55:39 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-07-20 15:44:13 +0200
commitecf880d0c50f7be9ab80893ae1fcc6714b3a2309 (patch)
tree1e1ce1849a8251c19415cffb21eb52f5d8581626 /test-suite/Makefile
parent2c5cc812d37da3f03abe3a0fb8029d1c74ad7b82 (diff)
fake_ide: do as coqide to find out coqtop path
Diffstat (limited to 'test-suite/Makefile')
-rw-r--r--test-suite/Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index a88fb6bc6..beb80a3df 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -446,7 +446,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake))
@echo "TEST $<"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(BIN)fake_ide $< "$(BIN)coqtop -coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off" 2>&1; \
+ $(BIN)fake_ide $< "-coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off" 2>&1; \
if [ $$? = 0 ]; then \
echo $(log_success); \
echo " $<...Ok"; \