Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

fix: inlay hints in untitled files #6978

Merged
merged 1 commit into from
Feb 6, 2025
Merged

fix: inlay hints in untitled files #6978

merged 1 commit into from
Feb 6, 2025

Conversation

mhuisi
Copy link
Contributor

@mhuisi mhuisi commented Feb 6, 2025 •
edited
Loading

This PR fixes a bug where both the inlay hint change invalidation logic and the inlay hint edit delay logic were broken in untitled files.
Thanks to @Julian for spotting this!

@mhuisi mhuisi added the changelog-server Language server, widgets, and IDE extensions label Feb 6, 2025
@mhuisi mhuisi enabled auto-merge February 6, 2025 19:12
@mhuisi mhuisi added this pull request to the merge queue Feb 6, 2025
@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 Feb 6, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 06d022b9c00d56b9a95a14449ee56bc080b2ab9d --onto b01ca8ee237a1b3c299384e73ad79d424e216a84. (2025-02-06 19:30:27)

Merged via the queue into leanprover:master with commit 45d3942 Feb 6, 2025
18 of 19 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
changelog-server Language server, widgets, and IDE extensions toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@mhuisi @leanprover-community-bot