Skip to content

Commit 5e32133

Browse files
authored
fix: non-LSP-compliant FileSystemWatcher (#10609)
This PR fixes an LSP-non-compliance in the `FileSystemWatcher` that was introduced in #925. Closes #10597.
1 parent b82303e commit 5e32133

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Lean/Data/Lsp/Workspace.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ structure WorkspaceFolder where
2929

3030
structure FileSystemWatcher where
3131
globPattern : String
32-
kind : Option Nat := none
32+
kind? : Option Nat := none
3333
deriving FromJson, ToJson
3434

3535
namespace FileSystemWatcher

0 commit comments

Comments
 (0)