equal
deleted
inserted
replaced
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()) |