| changeset 6541 | d3ac35b2bfbf |
| parent 3599 | 89cbba12863d |
| child 6657 | 9627197bd9e1 |
--- a/lib/browser/GraphBrowser/TreeNode.java Thu Apr 29 18:34:30 1999 +0200 +++ b/lib/browser/GraphBrowser/TreeNode.java Thu Apr 29 22:42:38 1999 +0200 @@ -33,7 +33,7 @@ public class TreeNode { - static Font f=new Font("Helvetica",Font.PLAIN,15); + static Font f=new Font("Helvetica", Font.PLAIN, 14); int starty,endy,number; String name,path;