Tue, 11 Jul 2023 19:18:27 +0200 suppress bad file, which does not work on regular Windows;
wenzelm [Tue, 11 Jul 2023 19:18:27 +0200] rev 78310
suppress bad file, which does not work on regular Windows;
Tue, 11 Jul 2023 18:30:56 +0200 revert ineffective b04ac8a017b2: etc/settings of polyml components needs to be changed as well;
wenzelm [Tue, 11 Jul 2023 18:30:56 +0200] rev 78309
revert ineffective b04ac8a017b2: etc/settings of polyml components needs to be changed as well;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 +300 +1000 tip