Zulip Chat Archive
Stream: mathlib4
Topic: pushed to master
Heather Macbeth (Jul 17 2023 at 18:24):
sorry!
Jireh Loreaux (Jul 17 2023 at 18:34):
Is a revert the right way to go here, or do we want to just rollback to 039dff725d0a2a4765c2d1b0dc12658969e2c826?
Jireh Loreaux (Jul 17 2023 at 18:35):
@maintainers
Johan Commelin (Jul 17 2023 at 18:35):
Force-pushing to a public master branch seems like a bad idea.
Chris Hughes (Jul 17 2023 at 18:35):
When I've done it I just revert the commit, so there will be a revert commit on the history to master and we don't worry about a dirty history
Jireh Loreaux (Jul 17 2023 at 18:36):
The offending commit is only 10 minutes old though, that's why I'm wondering.
Johan Commelin (Jul 17 2023 at 18:36):
Yeah, it's unlikely anybody pulled. But still...
Jireh Loreaux (Jul 17 2023 at 18:36):
Fair enough.
Last updated: Dec 20 2023 at 11:08 UTC