This would have reproduced the distcheck issue fixed in b2ad8d2a.
For the initial push of this MR, I've reverted b2ad8d2a to check that the error is really caught by CI. I'll remove that commit before marking this as non-draft.