torfason opened this issue 4 years ago · 1 comments
The changes in this branch are now in master, even if it has not formally been merged in. Deleting the branch would reduce ambiguity regarding that. Comments OK/pro/con would be appreciated.
Branch deleted.