From c03c379172277f7b7af41f00cd792fc58f9e7923 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Sun, 10 Sep 2023 12:38:30 +0200
Subject: [PATCH] codespaces config

---
 .devcontainer/devcontainer.json | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json
index 90d7155..8084f97 100644
--- a/.devcontainer/devcontainer.json
+++ b/.devcontainer/devcontainer.json
@@ -23,6 +23,9 @@
       "extensions": [
         "leanprover.lean4"
       ]
+    },
+    "codespaces": {
+      "openFiles": ["Game.lean"]
     }
   }
 }