Re: Change Font in Top Panel

[Martin Cigorraga <martincigorraga gmail com>]

Hey,

On Mon, Oct 19, 2015 at 5:57 AM, John Frankish <john frankish outlook com> wrote:

Hi Martin,

 

Thanks J

 

It took me a while to realise that I needed to recompile gnome-shell-extensions with ruby/sass installed to get User Themes, but after that it worked.

 

Ah, nice to know. I used to run more slimmer systems (or customizable/tweakable, if you like) but nowadays I'm fine with a distro that has a different approach to the way a system is built so I wasn't aware of that.

 

Does your tip actually change the top panel font or does it make the top panel smaller thus forcing the font to be smaller?

 

From what I understand what that setting does is instruct the Shell to use a predefined small size of whatever font you are using. Now it is beyond me what's exactly the size of the font is, I yet have to dig into GNOME Shell documentation... But if you have a couple of minutes and google that snippet of code you will find some posts that explains how it works - or at least I think so, I can't remember right now from where I took it.

 

BTW this also appeared to show that attempting to change fonts with the gnome-tweak-tool fonts/window title has no effect…

 

In my setup I can successfully change the type and size of the font used for the window title using GNOME Tweak Tool. Right now I'm using Cantarell 11 but it works with whatever font or size I choose.

 

Regards

John

Best!

-M.