--- a/src/Tools/GraphBrowser/GraphBrowser/Box.java Fri Jul 16 12:45:37 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-/***************************************************************************
- Title: GraphBrowser/Box.java
- Author: Gerwin Klein, TU Muenchen
-
- A box with width and height. Used instead of java.awt.Dimension for
- batch mode.
-
-***************************************************************************/
-
-package GraphBrowser;
-
-public class Box {
- public int width;
- public int height;
-
- public Box(int w, int h) {
- this.width = w;
- this.height = h;
- }
-}