Skip to content

Cannot input the unicode symbol ∂ with 'partial' #234

@leopold-gravier

Description

@leopold-gravier

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.

Image

This is the only character where I have an issue inputing it.

Steps to reproduce

  1. Enter input mode
  2. 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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething isn't working

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions