Thu, 31 Jan 2019 21:21:44 +0100 updated to polyml-test-1236652ebd55;
wenzelm [Thu, 31 Jan 2019 21:21:44 +0100] rev 69776
updated to polyml-test-1236652ebd55;
Thu, 31 Jan 2019 17:18:15 +0100 added option jedit_text_overview for visual appearance (not performance, see also 72216713733a);
wenzelm [Thu, 31 Jan 2019 17:18:15 +0100] rev 69775
added option jedit_text_overview for visual appearance (not performance, see also 72216713733a);
Thu, 31 Jan 2019 16:56:31 +0100 adapted to a8ee66876a1a;
wenzelm [Thu, 31 Jan 2019 16:56:31 +0100] rev 69774
adapted to a8ee66876a1a;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 tip