Commit 2023-03-12 16:37 6ceb5945
View on Github →chore: strip trailing spaces in lean files (#2828)
vscode is already configured by .vscode/settings.json
to trim these on save. It's not clear how they've managed to stick around.
By doing this all in one PR now, it avoids getting random whitespace diffs in PRs later.
This was done with a regex search in vscode,