src/Tools/jEdit/src/jedit/document_overview.scala
Tue, 08 Dec 2009 16:30:20 +0100 wenzelm misc modernization of names;
Tue, 08 Dec 2009 14:49:01 +0100 wenzelm misc rearrangement of files;
Tue, 15 Sep 2009 20:45:20 +0200 wenzelm renamed PhaseOverviewPanel to Document_Overview;
less more (0) tip