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