src/Tools/jEdit/jedit_main/scala_console.scala
Thu, 21 Apr 2022 11:28:50 +0200 wenzelm clarified signature;
Fri, 01 Apr 2022 23:19:12 +0200 wenzelm tuned formatting;
less more (0) -2 tip