src/Pure/Tools/doc.scala
Sun, 03 Apr 2016 22:31:16 +0200 wenzelm prefer internal tool;
Sun, 28 Feb 2016 17:40:01 +0100 wenzelm tuned signature;
less more (0) -10 -2 tip