src/Pure/Tools/scala_project.scala
Sat, 07 Mar 2020 12:15:15 +0100 wenzelm copy jEdit sources instead of jar, for better browsing experience;
Sun, 01 Mar 2020 22:52:46 +0100 wenzelm clarified command line;
less more (0) tip