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/21656 Group Owner: devel+ow...@edk2.groups.io Unsubscribe: https://edk2.groups.io/g/devel/unsub [arch...@mail-archive.com] -=-=-=-=-=-=-=-=-=-=-=-
