Merge branch 'master' of git.php.net:/php-src
authorFelipe Pena <felipensp@gmail.com>
Sat, 30 Nov 2013 13:41:23 +0000 (11:41 -0200)
committerFelipe Pena <felipensp@gmail.com>
Sat, 30 Nov 2013 13:41:23 +0000 (11:41 -0200)

Trivial merge