gitpod

2023-09-10 23:35:52 +02:00
parent f393706f93
commit 9766966db3
1 changed files with 1 additions and 3 deletions
--- a/.gitpod.yml
+++ b/.gitpod.yml
@@ -9,6 +9,4 @@ tasks:
  - before: |
      cd /workspace && git clone https://github.com/leanprover-community/lean4game.git && cd /workspace/lean4game && npm install
  - init: |
-      (lake update && lake exe cache get && lake build)
-  - command: |
-      cd /workspace/lean4game && export LEAN4GAME_SINGLE_GAME=true && npm start
+      lake update && lake exe cache get && lake build