raulcd commented on PR #13750: URL: https://github.com/apache/arrow/pull/13750#issuecomment-1226984744
Thanks @kevingurney for the detailed explanation. It seems you pushed to the branch a commit and history that was already on master. As there were no divergences between your branch and master GitHub marked that as merged as it was already on master. I am not entirely sure what would happen if you push new changes to that branch, maybe GitHub allows to reopen the PR but I do think creating a new PR is a good approach. -- This is an automated message from the Apache Git Service. To respond to the message, please log on to GitHub and use the URL above to go to the specific comment. To unsubscribe, e-mail: [email protected] For queries about this service, please contact Infrastructure at: [email protected]
