osdir.com


[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Issue with GitHub PR


hi,

On Mon, Oct 22, 2018 at 4:54 PM paddy horan <paddyhoran@xxxxxxxxxxx> wrote:

> Hey all,
>
> I created a PR for ARROW-3541, after addressing review comments i rebased
> and force pushed to my branch. GitHub seems to be having issues though, the
> PR is not updating and i don’t believe CI was re-triggered. Looking at the
> PR now comments I made this morning are not showing up and comments I
> deleted because GitHub posted them multiple times are back.
>
> I know we have tooling that relies on the PR name, for instance in JIRA
> the pull-request-available tag has been added to the issue.  Can I rename
> and abandon the PR so I can open a new PR with the correct name to try and
> get the CI to trigger or will this mess up our tooling?
>

github is having issues since Sunday:
-  https://status.github.com/messages

they are in the middle of recovering from them but in the meantime, they've
disabled webhooks.
I doubt resending a PR will work.

-s