back to plain name, to have it accepted my mysql;
authorwenzelm
Tue Nov 05 22:06:16 2019 +0100 (9 days ago ago)
changeset 7125327a998cdc0f4
parent 71252 b64fc38327ae
child 71254 ee3c43eb79ae
back to plain name, to have it accepted my mysql;
src/Pure/Tools/phabricator.scala
     1.1 --- a/src/Pure/Tools/phabricator.scala	Tue Nov 05 22:00:29 2019 +0100
     1.2 +++ b/src/Pure/Tools/phabricator.scala	Tue Nov 05 22:06:16 2019 +0100
     1.3 @@ -192,7 +192,7 @@
     1.4  
     1.5      progress.echo("MySQL setup...")
     1.6  
     1.7 -    File.write(Path.explode("/etc/mysql/mysql.conf.d/" + isabelle_phabricator_name(ext = "cnf")),
     1.8 +    File.write(Path.explode("/etc/mysql/mysql.conf.d/" + phabricator_name(ext = "cnf")),
     1.9  """[mysqld]
    1.10  max_allowed_packet = 32M
    1.11  innodb_buffer_pool_size = 1600M