src/Pure/General/mercurial.scala
changeset 68566 38c8b44b40b9
parent 67782 7e223a05e6d8
child 71312 937328d61436
equal deleted inserted replaced
68565:1b9462304e1d 68566:38c8b44b40b9
    86 
    86 
    87     def command(name: String, args: String = "", options: String = "",
    87     def command(name: String, args: String = "", options: String = "",
    88       repository: Boolean = true): Process_Result =
    88       repository: Boolean = true): Process_Result =
    89     {
    89     {
    90       val cmdline =
    90       val cmdline =
    91         "\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
    91         "export HGPLAIN=\n\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
    92           (if (repository) " --repository " + ssh.bash_path(root) else "") +
    92           (if (repository) " --repository " + ssh.bash_path(root) else "") +
    93           " --noninteractive " + name + " " + options + " " + args
    93           " --noninteractive " + name + " " + options + " " + args
    94       ssh.execute(cmdline)
    94       ssh.execute(cmdline)
    95     }
    95     }
    96 
    96