# HG changeset patch
# User wenzelm
# Date 1354110946 -3600
# Node ID 267bd685a69f930cf0f9dd52d8c6b39d0660e906
# Parent  3f0920f8a24eeb30ccb843424ffadb59abeed39f
smarter list layout;

diff -r 3f0920f8a24e -r 267bd685a69f src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Tue Nov 27 20:01:57 2012 +0100
+++ b/src/Tools/jEdit/src/session_dockable.scala	Wed Nov 28 14:55:46 2012 +0100
@@ -33,7 +33,8 @@
         if (index >= 0) jEdit.openFile(view, listData(index).node)
     }
   }
-  status.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
+  status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP)
+  status.peer.setVisibleRowCount(0)
   status.selection.intervalMode = ListView.IntervalMode.Single
 
   set_content(new ScrollPane(status))