Skip to content

Prevent history entries on every keystroke#112

Merged
joneugster merged 1 commit into
leanprover-community:mainfrom
frangio:patch-1
May 26, 2026
Merged

Prevent history entries on every keystroke#112
joneugster merged 1 commit into
leanprover-community:mainfrom
frangio:patch-1

Conversation

@frangio
Copy link
Copy Markdown
Contributor

@frangio frangio commented May 25, 2026

jotai-location defaults to pushState. As a result a new entry is added to the browser history on every change that impacts the URL, including keystrokes in the editor. replace: true uses replaceState instead and will update the current history entry.

Copy link
Copy Markdown
Collaborator

@joneugster joneugster left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

thanks!

@joneugster joneugster merged commit 5df72dc into leanprover-community:main May 26, 2026
5 checks passed
@frangio frangio deleted the patch-1 branch May 26, 2026 16:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants