I'm filing this because two different people have proposed different fixes for this, but there was no task to describe the problem.

Change 407416 had a related patch set uploaded (by Bartosz Dziewoński; owner: Esanders):
[mediawiki/core@master] Use inherited font size on inputWidget + editfont

https://gerrit.wikimedia.org/r/407416

Change 427049 had a related patch set uploaded (by Bartosz Dziewoński; owner: VolkerE):
[mediawiki/core@master] Bring textarea's on same max-width as other OOUI input widgets

https://gerrit.wikimedia.org/r/427049

Change 407416 merged by jenkins-bot:
[mediawiki/core@master] Fix width of OOUI TextInputWidget with .mw-editfont-... classes

https://gerrit.wikimedia.org/r/407416

Change 427049 abandoned by Esanders:
Bring textarea's on same max-width as other OOUI input widgets

Reason:
See I6a6757874a3502b42cff0a3edb55115a305ad609

https://gerrit.wikimedia.org/r/427049

Some "Git blame" led me here ;)

Could someone remember why we need to put "monospace" twice in the rule font-family: monospace, monospace; please?
I know it's some CSS workaround, but I cannot find any reference back…

Just found T176636 already.

Additional refs and explanation would still be welcome :)

font-family: monospace; makes browsers apply weird font-sizing calculations that don't follow standard CSS behavior, examples on a div (with 16px browser font-size):

• font-family: monospace; font-size:1em; will result in 13px font-size in Chromium browsers.
• font-family: monospace; font-size:0.8em; will result in 10.4px! (0.8 * 13px)
• a textarea without extra rules will have 13.3333px!
• a textarea with font-size:1em; rule will have 13px...

Any other font-family rule, ex. monospace, monospace; will disable this behavior.

Go-to article: http://code.iamkate.com/html-and-css/fixing-browsers-broken-monospace-font-handling/

Related: T182320: Fix textarea editor's edit font size