@mhb, the text size is an issue that was just fixed a few minutes ago when another branch was merged [1]. The work around will be updated a bit later today (7 or 8 hours from now) with similar changes.
[1] https://code.launchpad.net/~vthompson/ubuntu-terminal-app/fixes-1260903-button-text-size-color/+merge/199015
@mhb, the text size is an issue that was just fixed a few minutes ago when another branch was merged [1]. The work around will be updated a bit later today (7 or 8 hours from now) with similar changes.
[1] https:/ /code.launchpad .net/~vthompson /ubuntu- terminal- app/fixes- 1260903- button- text-size- color/+ merge/199015