Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
doc: clarify that
lean_initialize_runtime_module
is implied by `lea…
…n_initialize` (leanprover#6677) Calling both runs the initializers twice, resulting in a memory leak
- Loading branch information