# 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] =