jperp and jbot seem to elaborate to the same unicode

UniFormal / MMT

The MMT Language and System

https://uniformal.github.io/

Other

68 stars 23 forks source link

jperp and jbot seem to elaborate to the same unicode #478

Closed kohlhase closed 5 years ago

kohlhase commented 5 years ago

jperp should be U+27C2 jbot should be U+22A5 cc: @Jazzpirate

florian-rabe commented 5 years ago

I've changed it.

@kohlhase The info is stored in the file https://github.com/UniFormal/MMT devel/src/mmt-api/resources/unicode/unicode-latex-map which you can edit safely if you need more Unicode symbols in the future.

You need to reinstall the MMT plugin afterwards to make the change visible to jEdit. Not sure what to do for intelliJ.