We should maybe have done the grand renaming on a branch, so
that outside folks' stuff would still compile while we got
it all done? Next time one of us wants to make a sequence
of experimental changes, we should consider remote
branching...
Bart