From a8659be9548b62ed74ac36e43f5c73806f3955c8 Mon Sep 17 00:00:00 2001 From: Denis Gorbachev <829578+DenisGorbachev@users.noreply.github.com> Date: Tue, 15 Aug 2023 20:55:03 +0700 Subject: [PATCH] Add angle brackets to wordPattern --- vscode-lean4/language-configuration.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vscode-lean4/language-configuration.json b/vscode-lean4/language-configuration.json index e1d321e46..ed98e16bc 100644 --- a/vscode-lean4/language-configuration.json +++ b/vscode-lean4/language-configuration.json @@ -130,5 +130,5 @@ ["\"", "\""], ["'", "'"] ], - "wordPattern" : "([^`~@$%^&*()\\-=+\\[{\\]}⟨⟩⦃⦄⟦⟧⟮⟯‹›\\\\|;:\",./\\s]+)" + "wordPattern" : "([^`~@$%^&*()\\-=+\\[{\\]}⟨⟩⦃⦄⟦⟧⟮⟯‹›<>\\\\|;:\",./\\s]+)" }