[Mediawiki-l] Removing a custom namespace?

[Daniel Barrett]

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_custom_namespaces

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