updated devcontainer default open files

1 year ago · 400ea1ab85
parent 21d7d48b91
commit 400ea1ab85
1 changed files with 6 additions and 0 deletions
--- a/.devcontainer/devcontainer.json
+++ b/.devcontainer/devcontainer.json
@ -13,6 +13,12 @@
 			"extensions": [
 				"leanprover.lean4"
 			]
+		},
+		"codespaces": {
+			"openFiles": [
+				"Prova/MathlibExample.lean",
+				"Main.lean"
+			]
 		}
 	},
 	"postCreateCommand": [