Zulip Chat Archive
Stream: new members
Topic: PR - updated mathlib wrong and have 700 commits from others
Hannah Fechtner (Oct 25 2024 at 16:31):
I evidently did something wrong when updating mathlib for my PR#17195
Now it's got over 700 commits, mostly from other people. Does anyone know how I can get rid of those?
Daniel Weber (Oct 25 2024 at 16:32):
Yaël Dillies (Oct 25 2024 at 16:32):
Yaël Dillies (Oct 25 2024 at 16:33):
Do you know how to "rebase"?
Eric Wieser (Oct 25 2024 at 16:38):
This one was a github bug, fixed by toggling the base branch
Last updated: May 02 2025 at 03:31 UTC