Re: checkdoc (was: mh-e 6.2 imminent)

[Kim F. Storm]

Richard Stallman <address@hidden> writes:

>     Given Miles' statistics, that's +300 face names to be changed!
> 
>     Since some (many?) of those are user customizeable, changing their
>     name would be problematic -- so I suggest leaving things as they are!
> 
> We could make an alias mechanism for faces.

Yes, but I still feel we could spend our time better on other things
than renaming and creating aliases for 300+ faces -- if the _users_
will never see the difference (as Miles pointed out, customize adds
"Face" to the face name if its missing...

-- 
Kim F. Storm <address@hidden> http://www.cua.dk