Use default system font for terminal header titles

Authored by mglb on Jul 5 2019, 9:59 PM.

Description

Use default system font for terminal header titles

This is not only style change, but also a bugfix.
Header and title font was unspecified, so terminal monospace font was
used in most cases. However, when new split with different orientation
was created, the font of splitted terminal changed to the system font.

Steps to reproduce:

  • Split vertically - both titles use monospace font (propagated when
  • Split horizontally - splitted header's font changes to system default

Details

Committed
mglbJul 6 2019, 6:37 PM
Parents
R319:fb8890c1ac20: Merge branch 'gitlab/drag_drop_terminal_split' into 'master'
Branches
Unknown
Tags
Unknown