src/Tools/jEdit/jedit_main/scala_console.scala
Sat, 17 Jul 2021 23:09:54 +0200 wenzelm tuned --- based on hints by IntelliJ IDEA;
less more (0) -1 tip