From 0ede8f2c4c86bec2e1d9c049fd3a82d68ffa6fdc Mon Sep 17 00:00:00 2001 From: tydeu Date: Sun, 3 Oct 2021 17:09:30 -0400 Subject: [PATCH] chore; minor doc cleanup --- Lake/Package.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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).