diff --git a/.gitignore b/.gitignore index 1d60dbb262..59ebc302c5 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,5 @@ /build +produced.out result* # Do not commit the flake lockfile to avoid having to maintain it flake.lock diff --git a/Lake/CLI/Help.lean b/Lake/CLI/Help.lean index e3cc18e448..b738900017 100644 --- a/Lake/CLI/Help.lean +++ b/Lake/CLI/Help.lean @@ -163,7 +163,10 @@ USAGE: lake script run [/]