changeset 50473 | ca4088bf8365 |
parent 33686 | 8e33ca8832b1 |
--- a/lib/browser/GraphBrowser/DefaultFontMetrics.java Mon Dec 10 21:55:57 2012 +0100 +++ b/lib/browser/GraphBrowser/DefaultFontMetrics.java Tue Dec 11 10:35:42 2012 +0100 @@ -1,6 +1,7 @@ /*************************************************************************** Title: GraphBrowser/DefaultFontMetrics.java Author: Stefan Berghofer, TU Muenchen + Options: :tabSize=2: Default font metrics which is used when no graphics context is available (batch mode).