src/Pure/Tools/phabricator.scala
changeset 71284 49bc17bf4384
parent 71283 cfcc1a2233ca
child 71285 8cd05f7b3b4a
equal deleted inserted replaced
71283:cfcc1a2233ca 71284:49bc17bf4384
    74     init: String = "",
    74     init: String = "",
    75     body: String = "",
    75     body: String = "",
    76     exit: String = ""): String =
    76     exit: String = ""): String =
    77   {
    77   {
    78 """#!/bin/bash
    78 """#!/bin/bash
    79 
    79 """ + (if (init.nonEmpty) "\n" + init else "") + """
    80 {""" + (if (init.nonEmpty) "\n" + Library.prefix_lines("  ", init) else "") + """
    80 {
    81   while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
    81   while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
    82   do
    82   do
    83     NAME="$(echo "$REPLY" | cut -d: -f1)"
    83     NAME="$(echo "$REPLY" | cut -d: -f1)"
    84     ROOT="$(echo "$REPLY" | cut -d: -f2)"
    84     ROOT="$(echo "$REPLY" | cut -d: -f2)"
    85 """ + Library.prefix_lines("    ", body) + """
    85     {
    86   done""" +
    86 """ + Library.prefix_lines("      ", body) + """
    87     (if (exit.nonEmpty) "\n" + Library.prefix_lines("  ", exit) else "") + """
    87     } < /dev/null
    88 } < """ + File.bash_path(global_config) + """
    88   done
    89 """
    89 } < """ + File.bash_path(global_config) + "\n" +
       
    90     (if (exit.nonEmpty) "\n" + exit + "\n" else "")
    90   }
    91   }
    91 
    92 
    92   sealed case class Config(name: String, root: Path)
    93   sealed case class Config(name: String, root: Path)
    93   {
    94   {
    94     def home: Path = root + Path.explode(phabricator_name())
    95     def home: Path = root + Path.explode(phabricator_name())