Fri, 30 Dec 2022 21:09:50 +0100 proper thread context (amending 01a7265db76b) -- at the danger of blocking the GUI;
wenzelm [Fri, 30 Dec 2022 21:09:50 +0100] rev 76830
proper thread context (amending 01a7265db76b) -- at the danger of blocking the GUI;
Fri, 30 Dec 2022 20:38:29 +0100 more robust: avoid detour via somewhat fragile Node.Name.path;
wenzelm [Fri, 30 Dec 2022 20:38:29 +0100] rev 76829
more robust: avoid detour via somewhat fragile Node.Name.path;
Fri, 30 Dec 2022 20:26:28 +0100 clarified generic path operations;
wenzelm [Fri, 30 Dec 2022 20:26:28 +0100] rev 76828
clarified generic path operations;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 tip