# HG changeset patch
# User wenzelm
# Date 1706009315 -3600
# Node ID 0856026e2c88b092ee945e5f1475e6a4d3d00afc
# Parent  eeacad2a7aaaaa2ee6c0d439e81b227f061e364c
tuned whitespace in generated file;

diff -r eeacad2a7aaa -r 0856026e2c88 src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Tue Jan 23 12:28:02 2024 +0100
+++ b/src/Pure/Tools/phabricator.scala	Tue Jan 23 12:28:35 2024 +0100
@@ -87,8 +87,7 @@
 
     override def site_init(name: String, server_name: String, webroot: String): Unit = {
       File.write(site_conf(name),
-"""
-server {
+"""server {
   server_name """ + server_name + """;
   root """ + webroot + """;