I see increasing occurrences of trailing whitespaces in the dotty code base. This should be avoided since it messes up histories and diffs. 1. Everyone: Please configure your editor so that trailing whitespace are stripped on save 2. We should have a PR check that refuses to merge a PR if there is trailing whitespace We used to have that at some point, but it seems it's no longer active.