# HG changeset patch
# User wenzelm
# Date 1536340276 -7200
# Node ID 01f46a4b22b493b31ca30c09a88f729dedd025c9
# Parent  5129fcc1b6c09363d3a882fd2fdcdf84421ef8fd
tuned signature;

diff -r 5129fcc1b6c0 -r 01f46a4b22b4 src/Pure/System/process_result.scala
--- a/src/Pure/System/process_result.scala	Fri Sep 07 17:08:47 2018 +0200
+++ b/src/Pure/System/process_result.scala	Fri Sep 07 19:11:16 2018 +0200
@@ -23,6 +23,8 @@
   def ok: Boolean = rc == 0
   def interrupted: Boolean = rc == Exn.Interrupt.return_code
 
+  def error_rc: Process_Result = if (interrupted) this else copy(rc = rc max 1)
+
   def check_rc(pred: Int => Boolean): Process_Result =
     if (pred(rc)) this
     else if (interrupted) throw Exn.Interrupt()
diff -r 5129fcc1b6c0 -r 01f46a4b22b4 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Fri Sep 07 17:08:47 2018 +0200
+++ b/src/Pure/Tools/dump.scala	Fri Sep 07 19:11:16 2018 +0200
@@ -163,8 +163,7 @@
 
     Consumer.shutdown().foreach(progress.echo_error_message(_))
 
-    if (theories_result.ok) session_result
-    else session_result.copy(rc = session_result.rc max 1)
+    if (theories_result.ok) session_result else session_result.error_rc
   }