From 1881030c79eba7212fee24e330d8a5f8584175e3 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Mon, 27 May 2024 10:45:56 +0100
Subject: [PATCH] chore: add extensions.json to prevent pop-up about
 unnecessary extension

---
 user_repo_source/.vscode/extensions.json | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 user_repo_source/.vscode/extensions.json

diff --git a/user_repo_source/.vscode/extensions.json b/user_repo_source/.vscode/extensions.json
new file mode 100644
index 00000000..c40988e4
--- /dev/null
+++ b/user_repo_source/.vscode/extensions.json
@@ -0,0 +1,15 @@
+// This file prevents VS Code from making unhelpful suggestions about extensions
+// during the initial setup of Mathematics In Lean.
+{
+	// See https://go.microsoft.com/fwlink/?LinkId=827846 to learn about workspace recommendations.
+	// Extension identifier format: ${publisher}.${name}. Example: vscode.csharp
+
+	// List of extensions which should be recommended for users of this workspace.
+	"recommendations": [
+		"leanprover.lean4"
+	],
+	// List of extensions recommended by VS Code that should not be recommended for users of this workspace.
+	"unwantedRecommendations": [
+		"ms-vscode-remote.remote-containers"
+	]
+}