diff -r cfcc1a2233ca -r 49bc17bf4384 src/Pure/Tools/phabricator.scala --- a/src/Pure/Tools/phabricator.scala Mon Dec 16 13:58:46 2019 +0100 +++ b/src/Pure/Tools/phabricator.scala Mon Dec 16 15:18:03 2019 +0100 @@ -76,17 +76,18 @@ exit: String = ""): String = { """#!/bin/bash - -{""" + (if (init.nonEmpty) "\n" + Library.prefix_lines(" ", init) else "") + """ +""" + (if (init.nonEmpty) "\n" + init else "") + """ +{ while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; } do NAME="$(echo "$REPLY" | cut -d: -f1)" ROOT="$(echo "$REPLY" | cut -d: -f2)" -""" + Library.prefix_lines(" ", body) + """ - done""" + - (if (exit.nonEmpty) "\n" + Library.prefix_lines(" ", exit) else "") + """ -} < """ + File.bash_path(global_config) + """ -""" + { +""" + Library.prefix_lines(" ", body) + """ + } < /dev/null + done +} < """ + File.bash_path(global_config) + "\n" + + (if (exit.nonEmpty) "\n" + exit + "\n" else "") } sealed case class Config(name: String, root: Path)