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

chore; minor doc cleanup

Browse source
This commit is contained in:
tydeu 2021-10-03 17:09:30 -04:00
parent 8852c5e236
commit 0ede8f2c4c
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Lake/Package.lean
View file

@ -224,7 +224,7 @@ structure PackageConfig where
/--
The root module of the package's binary executable.
Defaults to `Main`.
Defaults to `defaultBinRoot` (i.e., `Main`).
The root is built by recursively building its
local imports (i.e., fellow modules of the package).