On 06/09/20 23:51, Laszlo Ersek wrote: > 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.
Yet another symptom is that the PR creation page is stuck at "Checking mergeability… Don’t worry, you can still create the pull request." So I would say that nothing AJAX-y is working at the moment. Thanks Laszlo -=-=-=-=-=-=-=-=-=-=-=- Groups.io Links: You receive all messages sent to this group. View/Reply Online (#60993): https://edk2.groups.io/g/devel/message/60993 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] -=-=-=-=-=-=-=-=-=-=-=-
