Mon, 17 Oct 2022 22:24:32 +0200 wenzelm more robust, e.g. for "isabelle dump";
Mon, 17 Oct 2022 20:24:15 +0200 wenzelm allow spaces in SCALA_HOME directory name;
Mon, 17 Oct 2022 20:18:05 +0200 wenzelm avoid spurious error messages, e.g. when scala is missing;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 tip