max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: non-LSP-compliant FileSystemWatcher (#10609)

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

Closes #10597.
This commit is contained in:
Marc Huisinga 2025-09-29 16:16:09 +02:00 • committed by GitHub
parent 239c348239
commit c016bb9434
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Data/Lsp/Workspace.lean
View file

@ -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