On 13/05/2023 11.14, Helmut Grohne wrote:
I noticed a suprising undeclared file conflict. While Andreas' tooling finds most of these, it missed this one. It's about
Actually I never considered looking for this class of bugs (directory vs. non-directory). Thanks for catching them!
Andreas
