lean4-htt/stage0
Sebastian Ullrich 582877d2d3
feat: environment extension data can be split into .olean.server (#7914)
This PR adds a function hook `PersistentEnvExtension.saveEntriesFn` that
can be used to store server-only metadata such as position information
and docstrings that should not affect (re)builds.
2025-04-11 13:06:19 +00:00
..
src feat: environment extension data can be split into .olean.server (#7914) 2025-04-11 13:06:19 +00:00
stdlib chore: update stage0 2025-04-10 12:26:07 +00:00