src/Pure/General/mercurial.scala
changeset 64028 6cc79f1c82cd
parent 64027 4a33d740c9dc
child 64033 2989c1f2593a
equal deleted inserted replaced
64027:4a33d740c9dc 64028:6cc79f1c82cd
    31     override def toString: String = root.toString
    31     override def toString: String = root.toString
    32 
    32 
    33     def close() { }
    33     def close() { }
    34 
    34 
    35     def command(cmd: String, cwd: JFile = null): Process_Result =
    35     def command(cmd: String, cwd: JFile = null): Process_Result =
    36       Isabelle_System.hg("--repository " + File.bash_path(root) + " " + cmd, cwd = cwd)
    36       Isabelle_System.hg("--repository " + File.bash_path(root) + " --noninteractive " + cmd,
       
    37         cwd = cwd)
    37 
    38 
    38 
    39 
    39     def heads(template: String = "{node|short}\n", options: String = ""): List[String] =
    40     def heads(template: String = "{node|short}\n", options: String = ""): List[String] =
    40       command("heads " + options + opt_template(template)).check.out_lines
    41       command("heads " + options + opt_template(template)).check.out_lines
    41 
    42