One possibility is that the APL385.ttf font entry for diamond is either wrong, or has some subtle problem that causes gnome-terminal to get the scaling wrong. The font is available here:
www.dyalog.com/downloads/fonts/Apl385.ttf
One possibility is that the APL385.ttf font entry for diamond is either wrong,
or has some subtle problem that causes gnome-terminal to get the scaling wrong.
The font is available here:
www.dyalog. com/downloads/ fonts/Apl385. ttf