From 83dffbc2f8357dd679cf0e96cac21e05052e6b37 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Dvo=C5=99=C3=A1k?= Date: Thu, 23 Feb 2023 18:14:17 +0100 Subject: [PATCH] doc: mention `lake clean` in README (leanprover/lake#156) --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 99a642e974..7a3ef4876b 100644 --- a/README.md +++ b/README.md @@ -92,7 +92,7 @@ lean_exe «hello» { } ``` -The command `lake build` can then be used to build the package (and its [dependencies](#adding-dependencies), if it has them) into a native executable. The result will be placed in `build/bin`. +The command `lake build` can then be used to build the package (and its [dependencies](#adding-dependencies), if it has them) into a native executable. The result will be placed in `build/bin`. The command `lake clean` deletes `build`. ``` $ lake build