# HG changeset patch # User wenzelm # Date 1572987976 -3600 # Node ID 27a998cdc0f4b39d42de83c599e1ba3969690150 # Parent b64fc38327aeb57502de9508d7a5db065c674b3c back to plain name, to have it accepted my mysql; diff -r b64fc38327ae -r 27a998cdc0f4 src/Pure/Tools/phabricator.scala --- a/src/Pure/Tools/phabricator.scala Tue Nov 05 22:00:29 2019 +0100 +++ b/src/Pure/Tools/phabricator.scala Tue Nov 05 22:06:16 2019 +0100 @@ -192,7 +192,7 @@ progress.echo("MySQL setup...") - File.write(Path.explode("/etc/mysql/mysql.conf.d/" + isabelle_phabricator_name(ext = "cnf")), + File.write(Path.explode("/etc/mysql/mysql.conf.d/" + phabricator_name(ext = "cnf")), """[mysqld] max_allowed_packet = 32M innodb_buffer_pool_size = 1600M