changeset 50473 | ca4088bf8365 |
parent 33686 | 8e33ca8832b1 |
--- a/lib/browser/GraphBrowser/GraphBrowser.java Mon Dec 10 21:55:57 2012 +0100 +++ b/lib/browser/GraphBrowser/GraphBrowser.java Tue Dec 11 10:35:42 2012 +0100 @@ -1,6 +1,7 @@ /*************************************************************************** Title: GraphBrowser/GraphBrowser.java Author: Stefan Berghofer, TU Muenchen + Options: :tabSize=4: This is the graph browser's main class. It contains the "main(...)" method, which is used for the stand-alone version, as well as