# 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