fix devcontainer

hhu-adam · Dec 1, 2023 · ad19f88 · ad19f88
1 parent 8d48ed4
commit ad19f88
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json
@@ -13,7 +13,9 @@
   "overrideCommand": true,
   "onCreateCommand": {
     "npm_install": "(cd ~/lean4game && npm install)",
-    "lake_build": "(cd ~/game && lake update -R && lake build"
+    // BUG: Apparently `&& lake exe cache get` was needed here because the update hook was broken.
+    // should been fixed in https://github.com/leanprover-community/mathlib4/pull/8755
+    "lake_build": "(cd ~/game && lake update -R && lake exe cache get && lake build)"
   },
   "postStartCommand": "cd ~/lean4game && export VITE_LEAN4GAME_SINGLE=true && npm start",
   "customizations": {