From 6395ba2b36acb3560e1dd336760b0449dd70ab98 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 27 Nov 2014 15:54:20 +0100
Subject: Fix test flags for fake_ide

---
 test-suite/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/Makefile b/test-suite/Makefile
index a676d89e70..7f6a8eb9e3 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -415,7 +415,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-always-delegate" 2>&1; \
+	  $(BIN)fake_ide $< "$(BIN)coqtop -boot -async-proofs on" 2>&1; \
 	  if [ $$? = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
-- 
cgit v1.2.3