github "update branch" button

Stream: mathlib4

[Ruben Van de Velde]

Github has a button that allows merging master into your branch from the web ui: https://docs.github.com/assets/cb-12049/mw-1440/images/help/pull_requests/pull-request-update-branch-with-dropdown.webp

Apparently this can be turned on by maintainers: https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/managing-suggestions-to-update-pull-request-branches

How do people feel about doing that?

[Eric Wieser]

My experience with this button in the past is that newcomers just overclick it, because the button is presented as something that needs fixing

[Eric Wieser]

And so it will just increase our CI load for little benefit

[Yaël Dillies]

I personally think that manual merging is one step which is very efficient at teaching people git

[Jon Eugster]

Could such a button be just on PRs with a merge-conflict label, or would it basically always be there (since master is moving fast)?

If it provided a very simple way to update a branch with a trivial merge conflict, that could be handy. If it's just permanently there, Eric's point might be outweighting that.

[Ruben Van de Velde]

Permanently is the only option as far as I'm aware

[Eric Wieser]

When there is a merge conflict, GitHub already offers such a button by default

[Ruben Van de Velde]

Oh huh, I must be blind

[Eric Wieser]

If the conflicts are messy, GitHub hides the button