# HG changeset patch # User wenzelm # Date 1573744054 -3600 # Node ID f79006c533b09b1acdf89d3e23c1f062f382c265 # Parent 0ad53b5f2bb167cd13eb9e3aa63f246c3928efbc clarified errors: PHP daemon can fail under odd circumstances; diff -r 0ad53b5f2bb1 -r f79006c533b0 src/Pure/Tools/phabricator.scala --- a/src/Pure/Tools/phabricator.scala Thu Nov 14 14:03:42 2019 +0100 +++ b/src/Pure/Tools/phabricator.scala Thu Nov 14 16:07:34 2019 +0100 @@ -354,10 +354,12 @@ Linux.service_restart("apache2") + progress.echo("\nWeb configuration via " + server_url) + /* PHP daemon */ - progress.echo("PHP daemon setup ...") + progress.echo("\nPHP daemon setup ...") config.execute("config set phd.user " + Bash.string(daemon_user)) config.execute("config set phd.log-directory /var/tmp/phd/" + @@ -373,7 +375,8 @@ Isabelle_System.chmod("755", phd_command) Isabelle_System.chown("root:root", phd_command) - Linux.service_install(phd_name, + try { + Linux.service_install(phd_name, """[Unit] Description=PHP daemon manager for Isabelle/Phabricator After=syslog.target network.target apache2.service mysql.service @@ -390,9 +393,12 @@ [Install] WantedBy=multi-user.target """) - - - progress.echo("\nDONE\nWeb configuration via " + server_url) + } + catch { + case ERROR(msg) => + progress.bash("bin/phd status", cwd = config.home.file, echo = true).check + error(msg) + } }