From 8d48ed4b399efbc154dc822a1efab9e11a10171c Mon Sep 17 00:00:00 2001 From: joneugster Date: Fri, 1 Dec 2023 13:04:32 +0100 Subject: [PATCH] update workflow --- .devcontainer/devcontainer.json | 2 +- lake-manifest.json | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index 30b038b..58dab42 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -13,7 +13,7 @@ "overrideCommand": true, "onCreateCommand": { "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", "customizations": { diff --git a/lake-manifest.json b/lake-manifest.json index fa2d501..3c7f598 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -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",