Please merge in latest ProtoQuill into community build

[deusaquilus]

Hi, I made a PR to merge in latest ProtoQuill into the community build here:
dotty-staging/protoquill#1

Could someone please merge this?
Sorry if this is the wrong place for requests like this. How should I do it in the future?

[smarter]

I've given you push access to that repo, so you can just push there then open a PR here to update the submodule commit. Just make sure to never push-force and overwrite existing commits since that would prevent existing commits from passing the CI.

[deusaquilus]

Okay. Thanks!
Should I open up the submodule commit against dotty or dotty-staging?

[smarter]

against this repo, lampepfl/dotty

[deusaquilus]

Okay, just opened. #12630
Thanks!

[deusaquilus]

@smarter Any chance you can approve my workflow in #12630 ?

[deusaquilus]

Working now. Thanks!

[deusaquilus]

@smarter I restarted the builds. Looks like I need approval again. Sorry