diff --git a/Lake/Package.lean b/Lake/Package.lean index 6729ecee6d..23be0bd27e 100644 --- a/Lake/Package.lean +++ b/Lake/Package.lean @@ -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 diff --git a/README.md b/README.md index 5d6c530c4e..1db8ea6259 100644 --- a/README.md +++ b/README.md @@ -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`.