Closed 0xdabbad00 closed 3 years ago
This can be merged @steiza
I accidentally added some more commits to the same PR instead of creating a new one, but this can still be merged. The additional changes fix a bug and then resolves #816.
This can be merged @steiza