From 628e5e281859fcbebc01dab16cf11e6cc3137ee3 Mon Sep 17 00:00:00 2001 From: tydeu Date: Thu, 30 Sep 2021 15:50:22 -0400 Subject: [PATCH] fix: only call `removeDirAll` if path exists --- Lake/Cli.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Lake/Cli.lean b/Lake/Cli.lean index f2e752e54a..05d7b6de74 100644 --- a/Lake/Cli.lean +++ b/Lake/Cli.lean @@ -20,8 +20,9 @@ def Package.run (script : String) (args : List String) (self : Package) : IO PUn else self.scripts.forM fun name _ => IO.println name -def Package.clean (self : Package) : IO PUnit := - IO.FS.removeDirAll self.buildDir +def Package.clean (self : Package) : IO PUnit := do + if (← self.buildDir.pathExists) then + IO.FS.removeDirAll self.buildDir -- # CLI