diff --git a/Lake/Package.lean b/Lake/Package.lean index 2d74b5b48f..a60808b21c 100644 --- a/Lake/Package.lean +++ b/Lake/Package.lean @@ -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).