lib/browser/GraphBrowser/NormalVertex.java

--- a/lib/browser/GraphBrowser/NormalVertex.java	Thu Apr 29 18:34:30 1999 +0200
+++ b/lib/browser/GraphBrowser/NormalVertex.java	Thu Apr 29 22:42:38 1999 +0200
@@ -138,7 +138,7 @@
 		g.setColor(Color.black);
 	}
 
-	public void PS(PrintStream p) {
+	public void PS(PrintWriter p) {
 		p.print(leftX()+" "+getY()+" "+gra.box_width+" "+
 		        gra.box_height+" (");
 		for (int i=0;i<label.length();i++)