From d279a4871fa641f9bc423404cf2797fd3c26426e Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 14 Dec 2023 08:58:21 +0000 Subject: [PATCH] chore: add the lean4 extension to the vscode workspace (#3059) This prompts users opening the workspace (on a new device) for the first time to install the lean extension # Summary Link to `RFC` or `bug` issue: N/A --- lean.code-workspace | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/lean.code-workspace b/lean.code-workspace index 2816a1150a..4aae65961a 100644 --- a/lean.code-workspace +++ b/lean.code-workspace @@ -48,5 +48,10 @@ } } ] + }, + "extensions": { + "recommendations": [ + "leanprover.lean4" + ] } }