update workflow
This commit is contained in:
@@ -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 -R && lake build)"
|
"lake_build": "(cd ~/game && lake update -R && lake build"
|
||||||
},
|
},
|
||||||
"postStartCommand": "cd ~/lean4game && export VITE_LEAN4GAME_SINGLE=true && npm start",
|
"postStartCommand": "cd ~/lean4game && export VITE_LEAN4GAME_SINGLE=true && npm start",
|
||||||
"customizations": {
|
"customizations": {
|
||||||
|
|||||||
@@ -1,24 +1,24 @@
|
|||||||
{"version": 7,
|
{"version": 7,
|
||||||
"packagesDir": ".lake/packages",
|
"packagesDir": ".lake/packages",
|
||||||
"packages":
|
"packages":
|
||||||
[{"url": "https://github.com/leanprover/std4.git",
|
[{"url": "https://github.com/leanprover-community/lean4game.git",
|
||||||
|
"type": "git",
|
||||||
|
"subDir": "server",
|
||||||
|
"rev": "241ef4b67a5c95e33a4101769bb34ae45a66b82c",
|
||||||
|
"name": "GameServer",
|
||||||
|
"manifestFile": "lake-manifest.json",
|
||||||
|
"inputRev": "v4.3.0-rc2",
|
||||||
|
"inherited": false,
|
||||||
|
"configFile": "lakefile.lean"},
|
||||||
|
{"url": "https://github.com/leanprover/std4",
|
||||||
"type": "git",
|
"type": "git",
|
||||||
"subDir": null,
|
"subDir": null,
|
||||||
"rev": "a652e09bd81bcb43ea132d64ecc16580b0c7fa50",
|
"rev": "a652e09bd81bcb43ea132d64ecc16580b0c7fa50",
|
||||||
"name": "std",
|
"name": "std",
|
||||||
"manifestFile": "lake-manifest.json",
|
"manifestFile": "lake-manifest.json",
|
||||||
"inputRev": "v4.3.0-rc2",
|
"inputRev": "main",
|
||||||
"inherited": true,
|
"inherited": true,
|
||||||
"configFile": "lakefile.lean"},
|
"configFile": "lakefile.lean"},
|
||||||
{"url": "https://github.com/leanprover-community/lean4game.git",
|
|
||||||
"type": "git",
|
|
||||||
"subDir": "server",
|
|
||||||
"rev": "8851cd8b1f795e7701179d9b3568e52fc6729824",
|
|
||||||
"name": "GameServer",
|
|
||||||
"manifestFile": "lake-manifest.json",
|
|
||||||
"inputRev": "v4.3.0-rc2",
|
|
||||||
"inherited": false,
|
|
||||||
"configFile": "lakefile.lean"},
|
|
||||||
{"url": "https://github.com/leanprover-community/quote4",
|
{"url": "https://github.com/leanprover-community/quote4",
|
||||||
"type": "git",
|
"type": "git",
|
||||||
"subDir": null,
|
"subDir": null,
|
||||||
|
|||||||
Reference in New Issue
Block a user