Am 05.01.20 um 09:58 schrieb Andreas Schwab:
> That contains a lot of spurious whitespace differences.

You are right, that is not intended. Sometimes muscle memory just
invokes my whitespace cleaner.

Corrected patch attached.