Théo Winterhalter
Théo Winterhalter
Sorry I wasn't clear enough. When I do `Cmd + Shift + P`, select _Agda Mode: Input Symbol_, and then type `bn`, it displays `ℕ`, but when I just type...
As you can see, this is the same for me.  I am on Mac OS X Yosemite 10.10.4 (14E11f) using the last...
Nope, it only does that with `Cmd-Shift-P`. I have one warning related to your package, but I am not sure it had something to do with the bug at hand...
Thanks, but I am afraid nothing have changed (except that you have fixed all the warnings).
I just updated to the last version of your package, and it still doesn't work. Am I the only one having this problem?
No, I have tested them, and they seem to work just fine. Apparently there is no keystroke on `\` (but writing the `\` itself of course), just one on `cmd-\`:...
Even better: ``` cson 'atom-text-editor.agda': 'alt-/': 'agda-mode:input-symbol' ``` This is the same combination as for `\` and it actually works. Thanks.
I don't think so, but it is hard to tell. Using the right alt doesn't change anything for me (it works with `alt-/` and doesn't with `\\`).
Hi. It worked last time and it still does. I think it's because of the trick we mentioned earlier but it's not that bad is it? It's true we could...
Maybe I forgot something but I don't know how to remove the key binding `alt-/` to test.