Can do that. Should it be part of this PR or a separate one after this one is merged?

Whichever you prefer. I'd have said this one given it'll introduce yet another set of changes that are probably best diffed from current master, but I don't really mind either way in practice, so if it's easier for you just do another one afterwards.

Tags p* are NOT releases, but probably pre-versions, or even nightly snapshots. Releases are v*.
It's probably fine, but noteworthy 🙂

OK, I didn't notice the release tags. But since these are just about once a year, I guess we want the latest thing and "risk" the consequences, right?

Yeah, I think we can "risk it" 🙂


Reply to this email directly, view it on GitHub, or unsubscribe.
You are receiving this because you are subscribed to this thread.Message ID: <geany/geany/pull/3859/c2105264206@github.com>