src/Tools/Graphview/layout.scala
Thu, 04 Mar 2021 15:41:46 +0100 wenzelm tuned --- fewer warnings;
Mon, 01 Mar 2021 22:26:33 +0100 wenzelm tuned --- silence odd warning;
Mon, 01 Mar 2021 19:41:52 +0100 wenzelm tuned --- fewer warnings;
less more (0) -30 -10 -3 tip