Re: Issue with GitHub PR
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:
they are in the middle of recovering from them but in the meantime, they've
I doubt resending a PR will work.