What happened to `set_option maxHeartbeats` in v4.25.0?

Stream: mathlib4

[Nick_adfor]

In the earlier version, set_option maxHeartbeats can be used, but I've tried to use it in the latest one, it gives me

Unscoped option maxHeartbeats is not allowed:
Please scope this to individual declarations, as in

set_option maxHeartbeats in
-- comment explaining why this is necessary
example : ... := ...


Note: This linter can be disabled with `set_option linter.style.setOption false`

[Eric Wieser]

This is a linter warning from mathlib, and as a warning you can ignore it

[Eric Wieser]

But it is telling you that it is bad practice to use anything other than the set_option maxHeartbeats ... in form, as that version makes clear which parts of your code are slow

[Eric Wieser]

The warning message probably could benefit from an extra ...