src/Tools/Code/code_scala.ML
Fri, 05 Apr 2024 17:47:09 +0200 wenzelm adjust generated Scala to make it work with scalac -old-syntax and -new-syntax, although the latter is not regularly tested;
less more (0) -100 -30 -10 -1 tip