devcontainer

.devcontainer/devcontainer.json

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

.vscode/tasks.json

@@ -25,7 +25,7 @@
       "id": "openSimpleBrowser",
       "type": "command",
       "command": "simpleBrowser.show",
-      "args": ["http://localhost:3000/#/g/local/game"]
+      "args": ["http://localhost:3000"]
     }
   ]
 }