phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

images folder might not exist

Browse Source
This commit is contained in:
Jon Eugster
2023-12-08 00:58:17 +01:00
parent 0e652256f8
commit d5697d052e
1 changed files with 12 additions and 11 deletions
Download Patch File Download Diff File Expand all files Collapse all files
server/GameServer/Commands.lean
+12 -11
View File
@@ -688,17 +688,18 @@ open IO.FS System FilePath in
/-- Copies the folder `images/` to `.lake/gamedata/images/` -/ /-- Copies the folder `images/` to `.lake/gamedata/images/` -/
def copyImages : IO Unit := do def copyImages : IO Unit := do
let target : FilePath := ".lake" / "gamedata" let target : FilePath := ".lake" / "gamedata"
for file in ← walkDir "images" do if ← FilePath.pathExists "images" then
let outFile := target.join file for file in ← walkDir "images" do
-- create the directories let outFile := target.join file
if ← file.isDir then -- create the directories
createDirAll outFile if ← file.isDir then
else createDirAll outFile
if let some parent := outFile.parent then else
createDirAll parent if let some parent := outFile.parent then
-- copy file createDirAll parent
let content ← readBinFile file -- copy file
writeBinFile outFile content let content ← readBinFile file
writeBinFile outFile content