# HG changeset patch
# User wenzelm
# Date 1477490645 -7200
# Node ID 50bcf976f276d6a7cc8a4ce731542b3908036c00
# Parent  5c5b9d945625c03b642c26023a17ac2ee5688fac
clarified hg push return code: 1 means "nothing to push";

diff -r 5c5b9d945625 -r 50bcf976f276 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Wed Oct 26 15:21:16 2016 +0200
+++ b/src/Pure/General/mercurial.scala	Wed Oct 26 16:04:05 2016 +0200
@@ -109,7 +109,7 @@
     def push(remote: String = "", rev: String = "", force: Boolean = false, options: String = "")
     {
       hg.command("push", opt_rev(rev) + opt_flag("--force", force) + optional(remote), options).
-        check
+        check_rc(rc => rc == 0 | rc == 1)
     }
 
     def pull(remote: String = "", rev: String = "", options: String = ""): Unit =
diff -r 5c5b9d945625 -r 50bcf976f276 src/Pure/System/process_result.scala
--- a/src/Pure/System/process_result.scala	Wed Oct 26 15:21:16 2016 +0200
+++ b/src/Pure/System/process_result.scala	Wed Oct 26 16:04:05 2016 +0200
@@ -22,11 +22,13 @@
   def ok: Boolean = rc == 0
   def interrupted: Boolean = rc == Exn.Interrupt.return_code
 
-  def check: Process_Result =
-    if (ok) this
+  def check_rc(pred: Int => Boolean): Process_Result =
+    if (pred(rc)) this
     else if (interrupted) throw Exn.Interrupt()
     else Exn.error(err)
 
+  def check: Process_Result = check_rc(_ == 0)
+
   def print: Process_Result =
   {
     Output.warning(err)