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.

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

cannot send control-n nor control-t so cannot play HoTT game #1

Open
rudi-cilibrasi opened this issue Nov 27, 2022 · 0 comments
Open

Comments

@rudi-cilibrasi
Copy link

Hi. Thanks for making this great project I have really enjoyed playing with agda through it. I was trying to play the HoTT game https://homotopytypetheory.org/2021/12/01/the-hott-game/ lately and got stuck on quest 0. The reason is that I cannot enter control-n nor control-t in my chrome browser in agdapad. The browser eats the keystroke as a command and opens a new window or tab. I wonder if it would be possible to create some sort of key remapping or other feature so that control-n and control-t can be entered into agdapad? That way I could do the normalization and finish quest 0 in the HoTT game.

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

No branches or pull requests

1 participant