What is the safest way to remove a custom namespace after all its articles have been
deleted? If we just remove it from $wgExtraNamespaces, there will still be database
entries (e.g., in the archive table) that reference the old namespace number, and I
don't know if this will cause problems or not.
The official documentation isn't much help:
http://www.mediawiki.org/wiki/Manual:Using_custom_namespaces#Removing_custo…
In the worst case, we can rename the namespace to "OBSOLETE" and make it
read-only, or play tricks with Apache redirects, etc., but I'd prefer something
cleaner. Thanks.
DanB