src/Tools/GraphBrowser/graphbrowser/GraphBrowser.java
Fri, 16 Jul 2021 12:59:10 +0200 wenzelm tuned --- fewer warnings;
Fri, 16 Jul 2021 12:55:02 +0200 wenzelm clarified names;
less more (0) tip