| changeset 13968 | 689868b99bde |
| parent 6541 | d3ac35b2bfbf |
| child 13973 | 9170772bf420 |
--- a/lib/browser/GraphBrowser/Graph.java Wed May 07 14:53:35 2003 +0200 +++ b/lib/browser/GraphBrowser/Graph.java Wed May 07 16:38:55 2003 +0200 @@ -195,7 +195,7 @@ h=w=Integer.MIN_VALUE; while (e1.hasMoreElements()) { - Dimension dim=((Vertex)(e1.nextElement())).getLabelSize(g); + Box dim=((Vertex)(e1.nextElement())).getLabelSize(g); h=Math.max(h,dim.height); w=Math.max(w,dim.width); }