author | wenzelm |
Mon, 03 Sep 2012 10:17:17 +0200 | |
changeset 49071 | c1ca931b3647 |
parent 49070 | f00fee6d21d4 |
child 49072 | 747835eb2782 |
--- a/src/Tools/jEdit/src/output_dockable.scala Mon Sep 03 09:15:58 2012 +0200 +++ b/src/Tools/jEdit/src/output_dockable.scala Mon Sep 03 10:17:17 2012 +0200 @@ -107,9 +107,9 @@ case _ => true }).toList html_panel.render(filtered_results) - case _ => + case _ => html_panel.render(Nil) } - case None => + case None => html_panel.render(Nil) } } }