# HG changeset patch # User wenzelm # Date 1475524394 -7200 # Node ID 6cc79f1c82cde0a0b068835ac55f5b75ddc745c7 # Parent 4a33d740c9dc9e77d9a628a41ffb9df003f965cf more robust; diff -r 4a33d740c9dc -r 6cc79f1c82cd src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Mon Oct 03 21:36:10 2016 +0200 +++ b/src/Pure/General/mercurial.scala Mon Oct 03 21:53:14 2016 +0200 @@ -33,7 +33,8 @@ def close() { } def command(cmd: String, cwd: JFile = null): Process_Result = - Isabelle_System.hg("--repository " + File.bash_path(root) + " " + cmd, cwd = cwd) + Isabelle_System.hg("--repository " + File.bash_path(root) + " --noninteractive " + cmd, + cwd = cwd) def heads(template: String = "{node|short}\n", options: String = ""): List[String] =