diff options
| author | Enrico Tassi | 2016-06-14 11:41:33 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-06-14 11:41:33 +0200 |
| commit | ad3d0ce65ea4debacc98b50f58a96338c7bffc5d (patch) | |
| tree | 684717e138e3d6b1cd4efaab66dd7263e0ff9da2 | |
| parent | fb8e41ba16f3d52faabff5737ecdd80eb4715e82 (diff) | |
test-suiet: run fake_id as before pr/173 was merged
| -rw-r--r-- | test-suite/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 91b8a4ed08..b9c27a2fcf 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -421,7 +421,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" 2>&1; \ + $(BIN)fake_ide $< "$(BIN)coqtop -boot -async-proofs on -async-proofs-tactic-error-resiliency off -async-proofs-command-error-resiliency off" 2>&1; \ if [ $$? = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ |