# HG changeset patch
# User wenzelm
# Date 1350042913 -7200
# Node ID 28d207ba9340b71aab1ad2ceee2ad5713775b644
# Parent  2bc5924b117facbae7e821621c9f2d09ef544733
no special treatment of errors inside goal forks without transaction id, to avoid duplication in plain build with sequential log, for example;

diff -r 2bc5924b117f -r 28d207ba9340 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Fri Oct 12 13:46:41 2012 +0200
+++ b/src/Pure/goal.ML	Fri Oct 12 13:55:13 2012 +0200
@@ -160,7 +160,7 @@
                 (case result of
                   Exn.Res _ => ()
                 | Exn.Exn exn =>
-                    if Exn.is_interrupt exn then ()
+                    if id = 0 orelse Exn.is_interrupt exn then ()
                     else
                       (status task [Isabelle_Markup.failed];
                        Output.report (Markup.markup_only Isabelle_Markup.bad);