images folder might not exist

leanprover-community · Dec 7, 2023 · d5697d0 · d5697d0
1 parent 0e65225
commit d5697d0
Showing 1 changed file with 12 additions and 11 deletions.
diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean
@@ -688,17 +688,18 @@ open IO.FS System FilePath in
 /-- Copies the folder `images/` to `.lake/gamedata/images/` -/
 def copyImages : IO Unit := do
   let target : FilePath := ".lake" / "gamedata"
-  for file in ← walkDir "images" do
-    let outFile := target.join file
-    -- create the directories
-    if ← file.isDir then
-      createDirAll outFile
-    else
-      if let some parent := outFile.parent then
-        createDirAll parent
-      -- copy file
-      let content ← readBinFile file
-      writeBinFile outFile content
+  if ← FilePath.pathExists "images" then
+    for file in ← walkDir "images" do
+      let outFile := target.join file
+      -- create the directories
+      if ← file.isDir then
+        createDirAll outFile
+      else
+        if let some parent := outFile.parent then
+          createDirAll parent
+        -- copy file
+        let content ← readBinFile file
+        writeBinFile outFile content