max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: include Lake.Load in core build (#10087)

Browse source 
This PR adds `Lake.Load` to core's Lake configuration to ensure it is
built. With the module system port, it was no longer transitively
imported.
This commit is contained in:
Mac Malone 2025-08-23 17:52:15 -04:00 • committed by GitHub
parent c9727c2d19
commit 902484988e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/lakefile.toml.in
View file

@ -63,7 +63,7 @@ globs = [
# Lake API imported by configuration files
"Lake",
# API only imported by `LakeMain` and the `lake` CLI
"Lake.CLI",
"Lake.CLI", "Lake.Load",
]
libName = "${LAKE_LIB_PREFIX}Lake"
defaultFacets = ["static", "static.export"]