src/Pure/PIDE/command.ML
changeset 68871 f5c76072db55
parent 68868 5f44ad150ed8
child 68874 cca5ca811714
     1.1 --- a/src/Pure/PIDE/command.ML	Sat Sep 01 18:39:36 2018 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Sat Sep 01 20:20:50 2018 +0200
     1.3 @@ -260,7 +260,7 @@
     1.4          let
     1.5            val _ = status tr Markup.failed;
     1.6            val _ = status tr Markup.finished;
     1.7 -          val _ = if null errs then (report tr (Markup.bad ()); Exn.interrupt ()) else ();
     1.8 +          val _ = if null errs then (status tr Markup.canceled; Exn.interrupt ()) else ();
     1.9          in {failed = true, command = tr, state = st} end
    1.10      | SOME st' =>
    1.11          let