Skip to content

Use a monospace font for arrows#2431

Merged
simonpoole merged 2 commits intomasterfrom improve_disambiguation_menu_formattingNov 5, 2023