Closed tajmone closed 3 years ago
PS: Could please change the repository settings to rebase
pull requests (instead of merging them) by default?
GitHub defaults to always creating a merge commit, but this pollutes the repository history, and destroys the original commit messages (also, obscures the contributor), which makes it real hard to track the project history when sifting through its commits.
This PR enforces on to PPL sources trimming white spaces, as discussed in #5.
.editorconfig
code style rules for PPL sources: enable`trim_trailing_whitespace
.*.ppl
sources to enforce consistent code styles accordingly: