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, image

Estimated changes