Hi, I’d just like to say that I successfully used Kyle’s first patch to get past the problem. Thank you!
I’m a bit lost: is there something we need to decide on to move this forward? (The issue has become a bit more pressing as origin/main is the new default on Github since a while.) -- Ricardo
