Closed pisv closed 11 months ago
Fixes #753.
I'd like to merge it in a day or two, assuming there are no objections. Although formally not required, a review would be welcome.
Fixes #753.