On 06/09/20 23:37, Laszlo Ersek wrote: > Hi, > > On 03/12/20 22:57, Michael D Kinney wrote: > >> The hub command is very flexible. What commands did you try? > > github again failed to accept the "push" label when I tried to set it. > > Unlike last time, the push label *is* offered to me in the small widget > to the right. When I click the label, it even gets a check mark. > However, the label isn't actually applied to the PR. No comment saying > "lersek set the 'push' label now" is generated, and the push label is > not displayed to the right, once the small search widget is closed. > > I tried both the WebUI: > > https://github.com/tianocore/edk2/pull/672 > > and then the "hub" utility (with "--labels push"): > > https://github.com/tianocore/edk2/pull/673 > > In either case, the "push" label didn't take. > > Frustrating. > >> 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? > > I'm quite certain this is not related to mergify, as mergify's role > would be in the end, when all the checks pass. Mergify correctly > interprets the absence of the "push" label. The problem is that github > does not add the label, in spite of my actions.
I should note that the "Preview" tab on the PR creation page also stopped working for me. I click it, and I can see my browser generating network traffic, and nothing happens. I'm 100% sure it's a github server side problem, as in the last few hours, I've successfully merged three other PRs (669 through 671). And, the Preview tab worked with each one of those fine. Meanwhile, <https://www.githubstatus.com/> claims everything is "Normal". :/ (I'm not going to file an issue report with github.com, because the last time I did so, namely ticket 592107 on March 7th, I got a response on *May* 14th.) Thanks Laszlo -=-=-=-=-=-=-=-=-=-=-=- Groups.io Links: You receive all messages sent to this group. View/Reply Online (#60991): https://edk2.groups.io/g/devel/message/60991 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] -=-=-=-=-=-=-=-=-=-=-=-
