src/Tools/Graphview/metrics.scala
Mon, 04 Nov 2024 21:05:11 +0100 wenzelm unused;
Mon, 04 Nov 2024 20:55:01 +0100 wenzelm clarified signature;
Fri, 01 Apr 2022 17:06:10 +0200 wenzelm clarified formatting, for the sake of scala3;
less more (0) -10 -3 tip