aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/Makefile
diff options
context:
space:
mode:
authorGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2014-07-23 17:24:18 +0200
committerGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2014-07-24 14:14:31 +0200
commitc15571e367cf4d75c9e4aac589170e0213e4fe3b (patch)
treeca12232b2b7c24d3e2a8e08491c6ca2c5da18034 /test-suite/Makefile
parent1774a87504945a6e8b8aa465297dce672364b8a4 (diff)
fixup fakeide test-suite
Diffstat (limited to 'test-suite/Makefile')
-rw-r--r--test-suite/Makefile4
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 211797251..81a556671 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -228,7 +228,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v
$(HIDE){ \
echo $(call log_intro,$<); \
$(coqc) "$*" $(call get_coq_prog_args,"$<") -async-proofs on \
- -async-proofs-worker-flags fallback-to-lazy-if-marshal-error=no,fallback-to-lazy-if-slave-dies=no \
+ -async-proofs-private-flags fallback-to-lazy-if-marshal-error=no,fallback-to-lazy-if-slave-dies=no \
$$opts 2>&1; R=$$?; times; \
if [ $$R = 0 ]; then \
echo $(log_success); \
@@ -425,7 +425,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake))
@echo "TEST $<"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(BIN)fake_ide $< "$(BIN)coqtop -boot -async-proofs on -async-proofs-worker-flags min-proof-length-to-delegate=0" 2>&1; \
+ $(BIN)fake_ide $< "$(BIN)coqtop -boot -async-proofs on -async-proofs-always-delegate" 2>&1; \
if [ $$? = 0 ]; then \
echo $(log_success); \
echo " $<...Ok"; \