Closed msimberg closed 4 months ago
Wouldn't be better to merge to master and then cherry-pick? Otherwise we lose the link in v0.5.0.
Either way. In the release procedure there is a merge-to-master step right now which would bring the link to master anyway, but I see you've commented about that. If you prefer I can:
* change the base of this PR to `master` * change the instructions in the release procedure to add the link to `master`, then cherry-pick ?
Yes. I would prefer in this way, such that we are sure that everything is tested and working in master
.
Updated base branch to master
.
Mhm... Why are github actions not starting?
Either way. In the release procedure there is a merge-to-master step right now which would bring the link to master anyway, but I see you've commented about that. If you prefer I can:
master
master
, then cherry-pick ?