# This file contains local changes, so we can leave php5.ini to the Debian
# default. It is not directly used by PHP, but the update-php.ini script
# ensures it is put into the php.ini for each different domain.