Maybe it was just covered by #7524 until now. /cc #5061 and @echo-oddly.
Also resolve minor nitpicks -- *during* the merge commit.