Closed LecrisUT closed 3 months ago
I fixed CI on master. Could you please rebase this PR?
Not from the github gui (there's an option in the top-level settings page to enable it). Either tomorrow or if you want to force push a rebase
It seems a rebase was not necessary for merging. Thanks for your contribution.
I should figure out how to get merge-queue. Looks really handy
Closes #1085