Changes for PHP 7#3

halojoy wants to merge 12 commits intoj2s:masterj2s/phppgadmin:masterfrom

halojoy:masterhalojoy/phppgadmin-for-PHP7:masterCopy head branch name to clipboard