I had made the change locally, so make check and make syntax-check
were successful, but forgot to add/commit. Unfortunately, git allows a
push when the local directory is dirty, so it didn't catch my mistake.