> Finally merged this patch to master. Thanks a lot, David. I can finally delete my private tree from all except my devel machine. -- Juliusz