Laszlo, I understand your frustration. Let's work on resolving these issues.
What browser are you using? I would like the reproduce that issue and report to GitHub. Do you a screen shot where the labels button is not visibe? Did you use the same branch name or a new branch name with the same set of commits? When I do a 2nd PR for the same content, I use a new branch name. The hub command is very flexible. What commands did you try? I want to root cause this issue. I suspect it is more related to Mergify than GitHub or Azure Pipelines. There is a state machine that is watching statuses and the sequence of actions you are using must be going into a state I did not test. Are you able to provide the sequences of steps that got the PR into a bad state and the approximate time between steps? Thanks, Mike > -----Original Message----- > From: devel@edk2.groups.io <devel@edk2.groups.io> On > Behalf Of Laszlo Ersek > Sent: Thursday, March 12, 2020 2:06 PM > To: Kinney, Michael D <michael.d.kin...@intel.com> > Cc: edk2-devel-groups-io <devel@edk2.groups.io>; Sean > Brogan <sean.bro...@microsoft.com> > Subject: [edk2-devel] github PRs keep breaking for me > > 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 (#55835): https://edk2.groups.io/g/devel/message/55835 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] -=-=-=-=-=-=-=-=-=-=-=-
