| changeset 68927 | 01f46a4b22b4 |
| parent 68926 | 5129fcc1b6c0 |
| child 68929 | 10cbb5d99081 |
--- 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 }