Closed qvalentin closed 11 months ago
@baptman21 can be merged, I guess?
Sure
Dammit I didn't see the * on the push, the CI runs twice on PRs now, for both events. I'll fix it and make it run on push only on master. See #12
*
@baptman21 can be merged, I guess?