I'm trying to enter the character '⁂', which is one of the asterisk variations. When I type "\asterisk" I am given the default asterisk but no option to enter a number. The keymap
seems to indicate that there should be a number of asterisks available, so I don't know where else this could be breaking down. Do you have any hints what I may be doing wrong, or could there be a bug somewhere?
Best regards,
Chris
PS: this extension is really really appreciated thanks so much!
banacorn
commented
3 years ago
Hello,
I'm trying to enter the character '⁂', which is one of the asterisk variations. When I type "\asterisk" I am given the default asterisk but no option to enter a number. The keymap
https://github.com/banacorn/agda-mode-vscode/blob/master/asset/keymap.js
seems to indicate that there should be a number of asterisks available, so I don't know where else this could be breaking down. Do you have any hints what I may be doing wrong, or could there be a bug somewhere?
Best regards,
Chris
PS: this extension is really really appreciated thanks so much!