build issue

Stream: lean4

[Reid Barton]

I'm getting this error when I try to build the current version:

/home/rwbarton/math/lean/lean4/stage0/src/runtime/io.cpp: In function ‘lean::object* lean::lean_io_get_num_heartbeats(lean::obj_arg)’:
/home/rwbarton/math/lean/lean4/stage0/src/runtime/io.cpp:416:47: error: ‘get_num_heartbeats’ was not declared in this scope; did you mean ‘lean_io_get_num_heartbeats’?
  416 |     return io_result_mk_ok(lean_uint64_to_nat(get_num_heartbeats()));
      |                                               ^~~~~~~~~~~~~~~~~~
      |                                               lean_io_get_num_heartbeats

Is this some bootstrapping issue?

[Reid Barton]

I'm going to see if it persists after make clean

[Reid Barton]

ok, seems like make clean fixed it