-
Notifications
You must be signed in to change notification settings - Fork 45
Open
Labels
bugSomething isn't workingSomething isn't working
Description
Description
I am trying to input the partial derivative character ∂ (U+2202) using the unicode input tool. We should obtain this character by typing 'partial'.
But when I type 'par', the word gets replaced by a newline, and all subsequent characters are ignored by the unicode input.
This is the only character where I have an issue inputing it.
Steps to reproduce
- Enter input mode
- Type "partial"
Setup
Windows 10
VSCode 1.100.3
agda-mode 0.5.7
Note
There is one workaround though, which is to copy the word "partial", enter input mode, then paste.
banacorn
Metadata
Metadata
Assignees
Labels
bugSomething isn't workingSomething isn't working