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