[edk2-devel] github PRs keep breaking for me

[Laszlo Ersek]

Hi Mike,

(1) github stopped supporting my browser. I can no longer apply the push
label using my current browser. The "hub" cmdline utility does not seem
to support adding just a label to an existing PR.

(2) github closed my PR as a personal build (due to lack of the "push"
label), and now it even denies me the option to reopen the pull request.
I deleted and re-pushed the (identical) branch, which github noticed in
the PR, but it still wouldn't re-launch the CI build, or honor the
"push" label.

CI is good, but github+mergify have turned the merging of valid patch
series from a 3-second git-push command into repeated half-hour
nightmares. Sorry for the strong words, I'm livid.

Laszlo


-=-=-=-=-=-=-=-=-=-=-=-
Groups.io Links: You receive all messages sent to this group.

View/Reply Online (#55832): https://edk2.groups.io/g/devel/message/55832
Mute This Topic: https://groups.io/mt/71912281/1813853
Group Owner: devel+owner at edk2.groups.io
Unsubscribe: https://edk2.groups.io/g/devel/unsub  [edk2-devel-archive at redhat.com]
-=-=-=-=-=-=-=-=-=-=-=-