Patched fonts not showing up on gnome-terminal

Question

I installed the patched font "Source Code Pro" from https://github.com/ryanoasis/nerd-fonts#option-3-install-script on my Ubuntu 18.10 box.

I can see the font showing up on the Fonts program (as SauceCodePro).

I want to set it as the font for GNOME Terminal app (Edit -> Preferences -> Custom Font), however this font doesn't show up.

I have tried running sudo fc-cache -fv ~/.local/share/fonts, as well as restarting my computer. I also tried reinstalling the gnome-terminal package, but no dice.

Does anyone have any suggestion for what I could do here?

Answer 1

Thanks to @egmont's link to https://askubuntu.com/questions/1046871/nerd-font-not-fond-in-terminal-profile/, I figured out a way to get around this, as mentioned in one of the comments in that post:

• Install GNOME Tweaks
• Set the system monospace font to "SauceCodePro Mono Regular"
• In the Terminal's Font Preference, I leave the Custom Font option unchecked, .i.e use system font.