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
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 th
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
On 3/13/20 11:27 AM, Laszlo Ersek wrote:
I checked the manual / command line help.
- The "hub pr" command provides listing and local fetch / checkout. So
it didn't apply to my case.
I don't know if it'll help, but it looks like there's a new 'gh'
application that GitHub's working on: https
what I did: while
github reported the deletion and restoration (in fact: re-pushing) of
the same branch, it wouldn't reopen the PR, and/or restart CI. So the
"push" label (set from my other browser meanwhile) didn't make a
difference. And I couldn't manually reopen the same P
On
> Behalf Of Laszlo Ersek
> Sent: Thursday, March 12, 2020 2:06 PM
> To: Kinney, Michael D
> Cc: edk2-devel-groups-io ; Sean
> Brogan
> Subject: [edk2-devel] github PRs keep breaking for me
>
> Hi Mike,
>
> (1) github stopped supporting my browser. I can no
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 eve
