zzrough / gs-extensions-drop-down-terminal

Drop Down Terminal extension for the Gnome Shell
https://extensions.gnome.org/extension/442/drop-down-terminal/
GNU General Public License v3.0
416 stars 91 forks source link

[Feature Request] Custom font for text #136

Open pedroadame opened 8 years ago

pedroadame commented 8 years ago

I use powerline fonts for my oh-my-zsh theme, and special icons cannot be displayed on drop-down terminal because of it lack of custom font settings.

seleccion_001

seleccion_003

vortex41 commented 8 years ago

Try changing system default monospace font. I achieved that using gnome-tweaktool

pedroadame commented 8 years ago

Worked perfectly @vortex41 I leave it open because I think it would need custom fonts, but this is a nice workaround.