author | wenzelm |
Sat, 21 Nov 2015 20:12:36 +0100 | |
changeset 61727 | 6f1a84d78865 |
parent 61726 | 04f8564d6983 |
child 61728 | 5f5ff1eab407 |
--- a/src/Tools/jEdit/src/rendering.scala Sat Nov 21 19:38:14 2015 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Sat Nov 21 20:12:36 2015 +0100 @@ -686,7 +686,7 @@ val (states, other) = results.iterator.map(_._2).filterNot(Protocol.is_result(_)).toList .partition(Protocol.is_state(_)) - if (options.bool("editor_output_state")) states ::: other else other + states ::: other }