equal
deleted
inserted
replaced
1 // replacement for java.awt.Dimension |
1 /*************************************************************************** |
|
2 Title: GraphBrowser/Box.java |
|
3 ID: $Id$ |
|
4 Author: Gerwin Klein, TU Muenchen |
|
5 Copyright 2003 TU Muenchen |
|
6 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
7 |
|
8 A box with width and height. Used instead of java.awt.Dimension for |
|
9 batch mode. |
|
10 |
|
11 ***************************************************************************/ |
2 |
12 |
3 package GraphBrowser; |
13 package GraphBrowser; |
4 |
14 |
5 public class Box { |
15 public class Box { |
6 public int width; |
16 public int width; |