Closed mwilck closed 1 year ago
Argh I mistakenly pushed this branch to develop
already. I meant to just push a few tags :-(
I am unable to undo this mistake because force-pushing is into develop
is not allowed, and I don't have the permissions to change that
I am sorry about that. @hedayat, please have a look; if you have the permissions, please force-push 359283a to develop
to undo my mistake.
If you're fine with these changes, we can of course leave develop
as-is. Otherwise, I guess we need to revert the changes.
Aha! :) I thought maybe you really needed to merge this one :D Sure, I'll review it soon.
LGTM :)
This PR contains a few minor fixes that I made while doing the GNOME 45 port, which I think we want to have on the main develop branch, too.