Zulip Chat Archive

Stream: graph theory

Topic: matchings


view this post on Zulip Alena Gusakov (Dec 02 2020 at 22:05):

Is there anything else I need to do to get #5156 approved? There were two suggestions that I put aside for later, should I just implement them now?

view this post on Zulip Alena Gusakov (Dec 03 2020 at 23:24):

Don't know where to ask this - do people typically keep working from a branch after a PR from it has been approved?

view this post on Zulip Mario Carneiro (Dec 03 2020 at 23:34):

github prefers that you don't

view this post on Zulip Alena Gusakov (Dec 03 2020 at 23:34):

gotcha

view this post on Zulip Mario Carneiro (Dec 03 2020 at 23:34):

the UI gets a little wonky if you try to reopen a PR or reuse a PR branch

view this post on Zulip Alena Gusakov (Dec 03 2020 at 23:35):

i was just thinking that it feels a bit wasteful to keep making new branches for PRs

view this post on Zulip Mario Carneiro (Dec 03 2020 at 23:35):

you can delete the old ones, you know

view this post on Zulip Alena Gusakov (Dec 03 2020 at 23:35):

this is true, but does that delete the comment history?

view this post on Zulip Mario Carneiro (Dec 03 2020 at 23:35):

no

view this post on Zulip Alena Gusakov (Dec 03 2020 at 23:35):

ah okay, then that works lol

view this post on Zulip Alena Gusakov (Dec 03 2020 at 23:36):

thanks

view this post on Zulip Mario Carneiro (Dec 03 2020 at 23:36):

although it may make it harder to track down the commits they are attached to

view this post on Zulip Mario Carneiro (Dec 03 2020 at 23:36):

but if they have been squash merged in it's not particularly important to retain them

view this post on Zulip Alena Gusakov (Dec 03 2020 at 23:36):

gotcha

view this post on Zulip Eric Wieser (Dec 03 2020 at 23:38):

Bors deletes merged branches anyway, doesn't it?

view this post on Zulip Alena Gusakov (Dec 03 2020 at 23:39):

https://github.com/leanprover-community/mathlib/tree/simple_graph_matching

view this post on Zulip Alena Gusakov (Dec 03 2020 at 23:39):

this one's still up

view this post on Zulip Mario Carneiro (Dec 03 2020 at 23:39):

what's the PR?

view this post on Zulip Alena Gusakov (Dec 03 2020 at 23:40):

without realizing it i committed Eric's suggestion at the bottom, and that seems to have done something weird

view this post on Zulip Eric Wieser (Dec 03 2020 at 23:40):

You sure you didn't put it back up after bors deleted it?

view this post on Zulip Alena Gusakov (Dec 03 2020 at 23:40):

I honestly have no clue

view this post on Zulip Mario Carneiro (Dec 03 2020 at 23:40):

20 commits ahead and 25 behind master sounds like a bad sign

view this post on Zulip Alena Gusakov (Dec 03 2020 at 23:40):

Maybe I did some weird branching or something

view this post on Zulip Alena Gusakov (Dec 03 2020 at 23:41):

the original commit is still good

view this post on Zulip Alena Gusakov (Dec 03 2020 at 23:42):

https://github.com/leanprover-community/mathlib/pull/5156

view this post on Zulip Alena Gusakov (Dec 03 2020 at 23:42):

here's the PR

view this post on Zulip Eric Wieser (Dec 03 2020 at 23:43):

I find the bors way of rebasing all PRs at merge time makes it really hard to work with branches that build on top of multiple open PRs, as you then have no easy way to merge in master when the PRs you depend on get in

view this post on Zulip Alena Gusakov (Dec 03 2020 at 23:43):

Nevermind, it wasn't the commit. I genuinely have no idea what happened there

view this post on Zulip Alena Gusakov (Dec 03 2020 at 23:43):

I might've just done something wrong accidentally because I was jumping back and forth between the two PRs I had open

view this post on Zulip Alena Gusakov (Dec 03 2020 at 23:44):

I can delete the branch maybe?

view this post on Zulip Mario Carneiro (Dec 03 2020 at 23:45):

you can delete it, but make sure you have everything you want to keep from it first

view this post on Zulip Alena Gusakov (Dec 03 2020 at 23:46):

Actually I think it's okay - it looks like the PR keeps the comment history

view this post on Zulip Alena Gusakov (Dec 03 2020 at 23:47):

To delete I mean


Last updated: May 08 2021 at 21:09 UTC