From b0bcb4af57ae3794c9ef763ca483bb2734bee6bd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 7 Jan 2017 10:39:57 -0800 Subject: [PATCH] chore(tests/lean/run/listex2): fix issue at travis, profiler option is not available in single thread build --- tests/lean/run/listex2.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/run/listex2.lean b/tests/lean/run/listex2.lean index d9fa14ace8..d1aae92d64 100644 --- a/tests/lean/run/listex2.lean +++ b/tests/lean/run/listex2.lean @@ -63,7 +63,7 @@ begin [smt] repeat {ematch} -- It will loop if there is a matching loop end -set_option profiler true +-- set_option profiler true /- Smaller problems can be solved using superposition in a reasonable amount of time. -/ example (a b c : nat) (l₁ l₂ : list nat) : a ∈ l₁ → a ∈ b::l₁ ++ [c] :=