is `trace.profiler.useHeartbeats` a thing?

Stream: lean4

[Kevin Buzzard]

On 4.9.0-rc3, a hover on the set_option trace.profiler.threshold says

threshold in milliseconds (or heartbeats if trace.profiler.useHeartbeats is true),
traces below threshold will not be activated

but

set_option trace.profiler.useHeartbeats true

gives

unknown option 'trace.profiler.useHeartbeats'

[Mauricio Collares]

Good catch, lean4#3986 introduced the option but there was a typo in its name (it's currently called trace.profiler.useHearbeats)

[Kyle Miller]

Thanks: lean4#4590