PHP error in server config edit form when old PHP versions are used

See comments in #5063 (closed) for details.