src/Pure/Tools/phabricator.scala
changeset 73736 a8ff6e4ee661
parent 73566 4e6b31ed7197
child 74944 9b14491ca5c6
--- a/src/Pure/Tools/phabricator.scala	Tue May 18 22:02:21 2021 +0200
+++ b/src/Pure/Tools/phabricator.scala	Wed May 19 10:41:28 2021 +0200
@@ -91,7 +91,7 @@
     NAME="$(echo "$REPLY" | cut -d: -f1)"
     ROOT="$(echo "$REPLY" | cut -d: -f2)"
     {
-""" + Library.prefix_lines("      ", body) + """
+""" + Library.indent_lines(6, body) + """
     } < /dev/null
   done
 } < """ + File.bash_path(global_config) + "\n" +