diff -r 0493188cff42 -r 4f24fd4dbcf5 lib/browser/GraphBrowser/Vertex.java
--- a/lib/browser/GraphBrowser/Vertex.java	Mon Oct 22 12:11:00 2001 +0200
+++ b/lib/browser/GraphBrowser/Vertex.java	Mon Oct 22 14:51:39 2001 +0200
@@ -2,7 +2,7 @@
   Title:      GraphBrowser/Vertex.java
   ID:         $Id$
   Author:     Stefan Berghofer, TU Muenchen
-  Copyright   1997  TU Muenchen
+  License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
   This class contains attributes and methods common to all kinds of
   vertices (e.g. coordinates, successors, predecessors).
@@ -15,8 +15,6 @@
 import java.io.*;
 
 abstract class Vertex {
-	protected static final Font font=new Font("Helvetica",Font.PLAIN,12);
-
 	Vector children=new Vector(10,10);
 	Vector parents=new Vector(10,10);
 	int degree=0;
@@ -70,7 +68,7 @@
 
 	public Dimension getLabelSize(Graphics g) {
 		FontMetrics fm = g == null ? 
-		    new DefaultFontMetrics(font) : g.getFontMetrics(font);
+		    new DefaultFontMetrics(12) : g.getFontMetrics(g.getFont());
 		
 		return new Dimension(
 		        Math.max(fm.stringWidth("[. . . .]"),fm.stringWidth(getLabel())),