Change oddly-chosen OID allocation.
I noticed while fooling with John Naylor's bootstrap-data patch that we had
one high-numbered manually assigned OID, 8888, which evidently came from a
submission that the committer didn't bother to bring into line with usual
OID allocation practices before committing. That's a bad idea, because it
creates a hazard for other patches that may be temporarily using high OID
numbers. Change it to something more in line with what we usually do.
This evidently dates to commit
abb173392. It's too late to change it
in released branches, but we can fix it in HEAD.