Originally we had commit 73d7fee2f31ade8e1a9c456c324255212c30c2a6 This worked for a while, but now the PR is no longer found by the github api for reasons we cannot fathom We are now using an even older commit, which currently works.