From 400ea1ab854800106feacfc0f500046bdeac255a Mon Sep 17 00:00:00 2001
From: Antonio De Lucreziis <antonio.delucreziis@gmail.com>
Date: Fri, 29 Sep 2023 20:01:31 +0200
Subject: [PATCH] updated devcontainer default open files

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

diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json
index ff2fbb6..b646519 100644
--- a/.devcontainer/devcontainer.json
+++ b/.devcontainer/devcontainer.json
@@ -13,6 +13,12 @@
 			"extensions": [
 				"leanprover.lean4"
 			]
+		},
+		"codespaces": {
+			"openFiles": [
+				"Prova/MathlibExample.lean",
+				"Main.lean"
+			]
 		}
 	},
 	"postCreateCommand": [