[gedit-list] Is the font size for Shell Output hard-coded?

[Amondo Roquentin <amondo globalstatic net>]

In gedit 2.24.2, I noticed that the Shell Output in the Bottom Pane has
an large font compared to the rest of my font settings.

I tried changing my desktop-wide font settings and also the font size in
the gedit preference.

But that did not affect the size of the font in the Shell Output tab.

Is the font size for the Shell Output tab really hard-coded or do I have
something set up incorrectly?

Do you think that the font size for the Shell Output tab should follow
the desktop-wide "Fixed width font" setting?