reverting commits

Stream: general

[Reid Barton]

When reverting commits, is there an established format for the commit message first line, or do we just use the one produced by git?

[Pedro Minicz]

I'd recommend squashing those commits before a pull request if that is the case. But the desired is probably to undo something already in the main repo, unfortunately I am unfamiliar with the conventions used here.

[Johan Commelin]

I think that whatever git produces is fine. And if you want to add details for why you are reverting, feel free to add.

[Johan Commelin]

Anyway, IIRC the revert-commit is now already merged into master (-;