This message was deleted.

Feel free to ignore it, we don’t have automation that would work for external PRs yet

OK so what would be the process to get the PR merged?