yet more test fixes

leanprover · Oct 1, 2024 · cf0c922 · cf0c922
1 parent c38214f
commit cf0c922
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 4 deletions.
diff --git a/tests/lean/run/3554.lean b/tests/lean/run/3554.lean
@@ -7,10 +7,6 @@ set_option debug.moduleNameAtTimeout false
 error: (deterministic) timeout, maximum number of heartbeats (100) has been reached
 Use `set_option maxHeartbeats <num>` to set the limit.
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
----
-error: (deterministic) timeout, maximum number of heartbeats (100) has been reached
-Use `set_option maxHeartbeats <num>` to set the limit.
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 set_option maxHeartbeats 100 in

diff --git a/tests/lean/tcloop.lean.expected.out b/tests/lean/tcloop.lean.expected.out
@@ -3,3 +3,4 @@ tcloop.lean:14:2-14:15: error: failed to synthesize
 (deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached
 Use `set_option synthInstance.maxHeartbeats <num>` to set the limit.
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Additional diagnostic information may be available using the `set_option diagnostics true` command.