[Cuis-dev] Alternative arrows

[Luciano Notarfrancesco]

What do you think about adding two preferences to set the unicode
characters to be used for displaying ^ and _? The problem I’m having is
that the arrows that we currently use are the same that are commonly used
in mathematics for morphisms, and the code gets a bit confusing in my
system, so I’d like to use the thick arrow 16r2B05 for _ and 16r2B06 for ^,
and to avoid annoying people who like the current arrows I think we could
make this a preference. Is this reasonable?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.cuis.st/mailman/archives/cuis-dev/attachments/20221006/cc88b6e4/attachment.htm>