-
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.
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
bugSomething isn't workingSomething isn't working
