From 4b7a98bc388f6cee4e86fd6ccb6c7cd9869c50bb Mon Sep 17 00:00:00 2001 From: tydeu Date: Thu, 16 Sep 2021 21:48:21 -0400 Subject: [PATCH] chore: replace `removeDirAll` with the proper function --- Lake/Cli.lean | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/Lake/Cli.lean b/Lake/Cli.lean index 9d2057b9f4..7ec1ddb6a4 100644 --- a/Lake/Cli.lean +++ b/Lake/Cli.lean @@ -20,12 +20,8 @@ def Package.run (script : String) (args : List String) (self : Package) : IO PUn else self.scripts.forM fun name _ => IO.println name --- Hack since Lean provides no methods to remove directories -def removeDirAll (path : System.FilePath) : IO PUnit := - Lake.proc {cmd := "rm", args := #["-rf", path.toString]} |>.run - def Package.clean (self : Package) : IO PUnit := - removeDirAll self.buildDir + IO.FS.removeDirAll self.buildDir -- # CLI