From 7ea84c5961da0a9fb80d2dc57e772bce5fe963a1 Mon Sep 17 00:00:00 2001 From: tydeu Date: Fri, 10 Jun 2022 16:13:55 -0400 Subject: [PATCH] doc: update `defaultFacet` description --- Lake/Config/Package.lean | 2 +- README.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean index d0f10c2401..f6ad0345eb 100644 --- a/Lake/Config/Package.lean +++ b/Lake/Config/Package.lean @@ -86,7 +86,7 @@ structure PackageConfig extends WorkspaceConfig where /-- The optional `PackageFacet` to build on a bare `lake build` of the package. - Can be one of `exe`, `leanLib`, `staticLib`, `sharedLib`. + Can be one of `exe`, `leanLib`, `staticLib`, `sharedLib`, or `none`. Defaults to `exe`. See `lake help build` for more info on build facets. **DEPRECATED:** diff --git a/README.md b/README.md index 744ba9704a..a567874899 100644 --- a/README.md +++ b/README.md @@ -117,7 +117,7 @@ Workspace options are shared across a package and its dependencies. * `moreLeanArgs`: An `Array` of additional arguments to pass to `lean` while compiling Lean source files. * `moreLeancArgs`: An `Array` of additional arguments to pass to `leanc` while compiling the C source files generated by `lean`. Lake already passes `-O3` and `-DNDEBUG` automatically, but you can change this by, for example, adding `-O0` and `-UNDEBUG`. * `moreLibTargets`: An `Array` of additional library `FileTarget`s (beyond the package's and its dependencies' Lean libraries) to build and link to the package's binaries (and to dependent packages' binaries). **DEPRECATED:** Use separate [`extern_lib`](#external-libraries) targets instead. -* `defaultFacet`: The `PackageFacet` to build on a bare `lake build` of the package. Can be one of `bin`, `staticLib`, `sharedLib`, or `oleans`. Defaults to `exe`. See `lake help build` for more info on build facets. **DEPRECATED:** Package facets will be removed in a future version of Lake. Use a separate [`lean_lib`](#lean-libraries) or [`lean_exe`](#binary-executables) default target instead. +* `defaultFacet`: The `PackageFacet` to build on a bare `lake build` of the package. Can be one of `exe`, `leanLib`, `staticLib`, `sharedLib`, or `none`. Defaults to `exe`. See `lake help build` for more info on build facets. **DEPRECATED:** Package facets will be removed in a future version of Lake. Use a separate [`lean_lib`](#lean-libraries) or [`lean_exe`](#binary-executables) default target instead. ## Defining Build Targets