Skip to content

Commit 92e6585

Browse files
committed
chore: fix test
1 parent 6cc3b36 commit 92e6585

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

tests/lean/run/grind_heartbeats.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ macro_rules
1212
| `(gen! $n:num) => `(op (f $n) (gen! $(Lean.quote (n.getNat - 1))))
1313

1414
/--
15-
trace: [grind.issues] (deterministic) timeout at `isDefEq`, maximum number of heartbeats (5000) has been reached
15+
trace: [grind.issues] (deterministic) timeout at `grind`, maximum number of heartbeats (5000) has been reached
1616
Use `set_option maxHeartbeats <num>` to set the limit.
1717
1818
Additional diagnostic information may be available using the `set_option diagnostics true` command.

0 commit comments

Comments
 (0)