Skip to content

Commit

Permalink
update workflow
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster committed Dec 1, 2023
1 parent 2d560b1 commit 214cf0f
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion .devcontainer/devcontainer.json
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@
"overrideCommand": true,
"onCreateCommand": {
"npm_install": "(cd ~/lean4game && npm install)",
"lake_build": "(cd ~/game && lake update -R && lake build)"
"lake_build": "(cd ~/game && lake update -R && lake build"
},
"postStartCommand": "cd ~/lean4game && export VITE_LEAN4GAME_SINGLE=true && npm start",
"customizations": {
Expand Down
2 changes: 1 addition & 1 deletion lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@
{"url": "https://github.com/leanprover-community/lean4game.git",
"type": "git",
"subDir": "server",
"rev": "8851cd8b1f795e7701179d9b3568e52fc6729824",
"rev": "622e9d389768e8abb5b3103a65d07165587a27ad",
"name": "GameServer",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.3.0-rc2",
Expand Down

0 comments on commit 214cf0f

Please sign in to comment.