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

chore: fix some overlooked docs

Browse source
This commit is contained in:
tydeu 2021-10-29 19:04:21 -04:00
parent ae43e5b2fb
commit 8a20cafebf
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Lake/Package.lean
View file

@ -175,7 +175,7 @@ structure PackageConfig extends WorkspaceConfig where
/--
The `PackageFacet` to build on a bare `lake build` of the package.
Can be one of `bin`, `staticLib`, or `oleans`. Defaults to `bin`.
Can be one of `bin`, `staticLib`, `sharedLib`, or `oleans`. Defaults to `bin`.
See `lake help build` for more info on build facets.
-/
defaultFacet : PackageFacet := PackageFacet.bin

2
README.md
View file

@ -97,7 +97,7 @@ Workspace options are shared across a package and its dependencies.
* `name` **(Required)**: The `Name` of the package.
* `dependencies`: An `Array` of the package's dependencies.
* `extraDepTarget`: An extra `OpaqueTarget` that should be built before the package. `OpaqueTarget.collectList/collectArray` can be used combine multiple extra targets into a single `extraDepTarget`.
* `defaultFacet`: The `PackageFacet` to build on a bare `lake build` of the package. Can be one of `bin`, `staticLib`, or `oleans`. Defaults to `bin`. See `lake help build` for more info on build facets.
* `defaultFacet`: The `PackageFacet` to build on a bare `lake build` of the package. Can be one of `bin`, `staticLib`, `sharedLib`, or `oleans`. Defaults to `bin`. See `lake help build` for more info on build facets.
* `moreServerArgs`: Additional arguments to pass to the Lean language server (i.e., `lean --server`) launched by `lake server`.
* `srcDir`: The directory containing the package's Lean source files. Defaults to the package's directory. (This will be passed to `lean` as the `-R` option.)
* `buildDir`: The directory to which Lake should output the package's build results. Defaults to `build`.