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

editor/code: scope keybinding alt+enter correctly #188

Merged
merged 3 commits into from
Jan 18, 2023
Merged

editor/code: scope keybinding alt+enter correctly #188

merged 3 commits into from
Jan 18, 2023

Commits on Jan 18, 2023

  1. editor/code: scope keybinding alt+enter correctly 

    The keybinding alt+enter is also used in find-and-replace, when the user
wants to replace all instances. Before this change, the keybinding
supplied by coq-lsp used to interfere. Moreover, the keybinding should
be scoped for just the coq language.
    @artagnon
    artagnon committed Jan 18, 2023
    Configuration menu
    Copy the full SHA
    4269fe1 View commit details
    Browse the repository at this point in the history

  2. CHANGES: add entry for keybinding scope change

    @artagnon
    artagnon committed Jan 18, 2023
    Configuration menu
    Copy the full SHA
    bd09239 View commit details
    Browse the repository at this point in the history

  3. CHANGES: fix typo 

    Co-authored-by: Ali Caglayan <alizter@gmail.com>
    @artagnon @Alizter
    artagnon and Alizter committed Jan 18, 2023
    Configuration menu
    Copy the full SHA
    fd42ad8 View commit details
    Browse the repository at this point in the history