From 62ece342f56380e54ecfe2b403159e9b115a8406 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 21 Dec 2018 15:11:17 +0100
Subject: Test ltacprof in sequential mode

Scripting these commands in async mode does not really make sense.
---
 test-suite/output-modulo-time/ltacprof_cutoff.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v
index ae5d51bae8..b7c98aa134 100644
--- a/test-suite/output-modulo-time/ltacprof_cutoff.v
+++ b/test-suite/output-modulo-time/ltacprof_cutoff.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-profile-ltac") -*- *)
+(* -*- coq-prog-args: ("-async-proofs" "off" "-profile-ltac") -*- *)
 Require Coq.ZArith.BinInt.
 Module WithIdTac.
   Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac).
-- 
cgit v1.2.3