Skip to content

fix: version numbers in code actions#2721

Merged
kim-em merged 1 commit intoleanprover:masterfrom
bustercopley:code-action-document-version
Oct 24, 2023
Merged

fix: version numbers in code actions#2721
kim-em merged 1 commit intoleanprover:masterfrom
bustercopley:code-action-document-version

Conversation

@bustercopley
Copy link
Copy Markdown
Contributor

See Zulip topic, #306(Std).

VS Code ignores the version number in a WorkspaceEdit but does not allow it to be null. There is at least one LSP client which does validate the version number, namely the Eglot client included in Emacs. By sending the correct version, we can be compatible with both.

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Oct 20, 2023
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Oct 20, 2023
@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Oct 20, 2023
@ghost
Copy link
Copy Markdown

ghost commented Oct 20, 2023

kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 22, 2023
@kim-em kim-em removed the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Oct 24, 2023
@kim-em kim-em merged commit bccbefd into leanprover:master Oct 24, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants