Hey @laloch -- I set up the github actions to only trigger on push for a reason I can't remember, I think that's why they aren't triggering. You can either push up an empty commit, or we can try to add PRs to the list of trigger actions

I can try again, I did several pushes the last time and it didn't trigger the CI anyway.

You see? No CI for me 😞

Let's just get this merged. I wonder @gforsyth if this is related to the fact that @laloch id pushing from a fork

It shouldn't, but I'll see if we need to add anything else to the config

It's no problem for me to keep testing.

Yeah, but I want to cut a release today, and don't want to mix these two issues 😉

So, now with #3511 merged in, should I try one last time and rebase to master?

So, now with #3511 merged in, should I try one last time and rebase to master?

I would close and open one more new PR, and if that doesn't work, we'll just merge it

@gforsyth, OK, let's do it.
Closing to reopen in yet another PR.