lib/browser/GraphBrowser/Box.java

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/browser/GraphBrowser/Box.java	Wed May 07 16:38:55 2003 +0200
@@ -0,0 +1,13 @@
+// replacement for java.awt.Dimension
+
+package GraphBrowser;
+
+public class Box {
+  public int width;
+  public int height;
+
+  public Box(int w, int h) {
+    this.width = w;
+    this.height = h;
+  }
+}