Am Tue, Feb 28, 2023 at 09:55:28PM +0100 schrieb Andreas Enge: > Am Tue, Feb 28, 2023 at 09:51:49PM +0100 schrieb Andreas Enge: > > Maybe it is time to merge master back into core-updates? > Where the vague "it is time to" could be read as "could you please?". > It is something I have never done, so it makes me nervous. Well, I suppose > I could just merge and try to fix the merge conflicts?
Well, I gave it a try, and it seems to be okay. So far I pushed it as a separate branch, wip-andreas-merge. It does compile. If you agree, I could also push it to core-updates (assuming that merge commits can be pushed just like every other commit; I am a bit doubtful what happens if someone else pushes other commits in the meantime; probably then I will have to merge a second time, to core-updates, instead of just pushing there?). Andreas
