From ffd79a08243ba865ff521c3302e540d472e9291f Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Mon, 30 Oct 2023 12:09:51 -0400
Subject: [PATCH] fix: lake: ensure `untar` output directory exists

---
 src/lake/Lake/Build/Actions.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/lake/Lake/Build/Actions.lean b/src/lake/Lake/Build/Actions.lean
index 23fdd66554..20c0145897 100644
--- a/src/lake/Lake/Build/Actions.lean
+++ b/src/lake/Lake/Build/Actions.lean
@@ -99,6 +99,7 @@ def download (name : String) (url : String) (file : FilePath) : LogIO PUnit := d
 /-- Unpack an archive `file` using `tar` into the directory `dir`. -/
 def untar (name : String) (file : FilePath) (dir : FilePath) (gzip := true) : LogIO PUnit := do
   logVerbose s!"Unpacking {name}"
+  IO.FS.createDirAll dir
   let mut opts := "-x"
   if (← getIsVerbose) then
     opts := opts.push 'v'