diff -r 26cd26aaf108 -r a8ff6e4ee661 src/Pure/Tools/phabricator.scala --- 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" +