banacorn / agda-mode-vscode

agda-mode on VS Code
https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode
MIT License
170 stars 41 forks source link

do not use ctrl+u with terminal focus #60

Closed cspollard closed 3 years ago

cspollard commented 3 years ago

These changes prevent agda mode from "eating" ctrl+u before it makes it to the terminal!

I'm sorry I don't know how to test this locally, but I've made these local changes to my shortcuts file and achieved the desired behavior.

banacorn commented 3 years ago

Thanks, this looks great!