src/Pure/PIDE/protocol.scala
changeset 50507 9605b0d93d1e
parent 50501 6f41f1646617
child 51293 05b1bbae748d
     1.1 --- a/src/Pure/PIDE/protocol.scala	Thu Dec 13 19:53:55 2012 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Fri Dec 14 12:09:08 2012 +0100
     1.3 @@ -106,7 +106,7 @@
     1.4          val status = command_status(st.status)
     1.5          if (status.is_running) running += 1
     1.6          else if (status.is_finished) {
     1.7 -          if (st.results.exists(p => is_warning(p._2))) warned += 1
     1.8 +          if (st.results.entries.exists(p => is_warning(p._2))) warned += 1
     1.9            else finished += 1
    1.10          }
    1.11          else if (status.is_failed) failed += 1