From c016bb9434ca898a60b5a93a962393a204408d3d Mon Sep 17 00:00:00 2001
From: Marc Huisinga <mhuisi@protonmail.com>
Date: Mon, 29 Sep 2025 16:16:09 +0200
Subject: [PATCH] fix: non-LSP-compliant `FileSystemWatcher` (#10609)

This PR fixes an LSP-non-compliance in the `FileSystemWatcher` that was
introduced in #925.

Closes #10597.
---
 src/Lean/Data/Lsp/Workspace.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Data/Lsp/Workspace.lean b/src/Lean/Data/Lsp/Workspace.lean
index 8f22f920fc..dcf7e3ec37 100644
--- a/src/Lean/Data/Lsp/Workspace.lean
+++ b/src/Lean/Data/Lsp/Workspace.lean
@@ -29,7 +29,7 @@ structure WorkspaceFolder where
 
 structure FileSystemWatcher where
   globPattern : String
-  kind : Option Nat := none
+  kind? : Option Nat := none
   deriving FromJson, ToJson
 
 namespace FileSystemWatcher