src/Tools/jEdit/src/jedit/output_dockable.scala
changeset 34832 d785f72ef388
parent 34824 ac35eee85f5c
child 34867 d0057d9777ce
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Sun Jan 03 19:53:58 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Sun Jan 03 20:50:07 2010 +0100
@@ -40,7 +40,7 @@
             case Some(model) =>
               val body =
                 if (cmd == null) Nil  // FIXME ??
-                else cmd.results(model.recent_document)
+                else model.recent_document.current_state(cmd).results
               html_panel.render(body)
           }