# HG changeset patch # User wenzelm # Date 1573768760 -3600 # Node ID 781b15f53098f6c538b8d018def40659c80c0c93 # Parent 81536e5d8ea7ccc6a275e93bb9b655fdff13b861 more packages; diff -r 81536e5d8ea7 -r 781b15f53098 src/Pure/Tools/phabricator.scala --- a/src/Pure/Tools/phabricator.scala Thu Nov 14 22:37:12 2019 +0100 +++ b/src/Pure/Tools/phabricator.scala Thu Nov 14 22:59:20 2019 +0100 @@ -27,7 +27,7 @@ "git", "mysql-server", "apache2", "libapache2-mod-php", "php", "php-mysql", "php-gd", "php-curl", "php-apcu", "php-cli", "php-json", "php-mbstring", // more packages - "php-zip", "python-pygments", "ssh") + "php-zip", "python-pygments", "ssh", "subversion", "mercurial") /* global system resources */