greg/NNG
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

lake update

Browse Source
This commit is contained in:
Jon Eugster
2023-09-10 21:16:30 +02:00
parent 120c5ac6f4
commit c58eaf35a4
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
.devcontainer/devcontainer.json
View File

@@ -13,7 +13,7 @@
"overrideCommand": true, "overrideCommand": true,
"onCreateCommand": { "onCreateCommand": {
"npm_install": "(cd ~/lean4game && npm install)", "npm_install": "(cd ~/lean4game && npm install)",
"lake_build": "(cd ~/game && lake clean && lake exe cache get && lake build)" "lake_build": "(cd ~/game && lake update && lake exe cache get && lake build)"
}, },
"postStartCommand": "cd ~/lean4game && export LEAN4GAME_SINGLE_GAME=true && npm start", "postStartCommand": "cd ~/lean4game && export LEAN4GAME_SINGLE_GAME=true && npm start",
"customizations": { "customizations": {