* drop the ondrej/php PPA since PHP 7.x is available directly from Ubuntu 18.04 * intall PHP 7.2 which is just the "php" package in Ubuntu 18.04 * some package names changed, some unnecessary packages are no longer provided * update paths
ae8cd4ef