Merged! My second PR got merged into the upstream. I’m really proud of what I did, even if the change took only 19 minutes to code and test.

The change wasn’t that hard to make, thanks to the fact the main contributor allowed for coping generated files instead of linking them.