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;
less more (0) -1 tip