banacorn / agda-mode-vscode

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

Many Unicode input sequences no longer work #176

Closed szumixie closed 8 months ago

szumixie commented 8 months ago

Many Unicode input sequences such as \Gl no longer work since v0.4.5, they seem to have been removed in f8ae83e3224fd861affe6fa542e4e22029bfe662, even though they are still listed in agda-input.el.

banacorn commented 8 months ago

thanks!!!