[Cuis-dev] Alternative arrows

[Gerald Klix]

Luciano,

I see your problem,
but these Characters only have glyphs in the
DejaVu, JetBrainsMono, KiwiMaru and KurintoSans fonts.

To make this work properly, we need some means
to discover the aforementioned situation
and switch back to the current behavior.


Sorry and HTH,

Gerald


On 06.10.22 12:55, Luciano Notarfrancesco via Cuis-dev wrote:
> 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?
> 
>