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" +