Commit 2023-07-04 16:14 c795bd35

View on Github →

chore: remove occurrences of semicolon after space (#5713) This is the second half of the changes originally in #5699, removing all occurrences of ; after a space and implementing a linter rule to enforce it. In most cases this 2-character substring has a space after it, so the following command was run first:

find . -type f -name "*.lean" -exec sed -i -E 's/ ; /; /g' {} \;

The remaining cases were few enough in number that they were done manually.

Estimated changes