Skip to content

fix: include identifier before cursor in document highlight request#5237

Merged
mhuisi merged 2 commits intoleanprover:masterfrom mhuisi:mhuisi/broken-document-highlightSep 4, 2024
+3-3

Commits

Commits on Sep 2, 2024