/cc @adambaratz

Thanks for the PR. Could you close this and create a new one against the PHP-7.0 branch? master is 7.2, which is still a ways away from being released. It would be nice to get this fix out sooner.

@adambaratz Unless code has diverged, it's easy to apply PRs to a different branch by wget https://github.com/php/php-src/pull/2134.patch and git am 2134.patch. This is how I usually merge PRs :)

@nikic since a few weeks the person which generated the PR can also do this via webinterface on github.
see https://github.com/blog/2224-change-the-base-branch-of-a-pull-request

@staabm I tried that before (see the history on this PR) -- but this still requires rebasing the changes to a different branch first. Just changing it in the web interface will include all other commits to master in the PR as well ^^

Hi @nikic @adambaratz @staabm

Thank you for considering my PR. I have updated the base branch to PHP-7.0, please let me know if you need anything else.

Peter

I merged this successfully via @nikic's method. Thanks all. There's a JS error on the PR tool. I'll close this once it's working again.

Comment on behalf of adambaratz at php.net:

Merged into PHP-7.0 and up.

@adambaratz if there is a js error then please report it at bugs.php.net :)

Was nothing. Just had to clear cache...