src/Tools/Code/code_scala.ML
Sat, 05 Nov 2016 14:35:40 +0100 wenzelm Scala "\u" notation uses hexadecimal, not octal (amending 00a135c0a17f);
less more (0) -100 -30 -10 -1 tip