I think 3 and a half years is long enough for the redirection to be left around

diff --git a/maintenance/dumpHTML.php b/maintenance/dumpHTML.php
deleted file mode 100644 (file)
index bd94958..0000000
--- a/maintenance/dumpHTML.php
+++ /dev/null
@@ -1,7 +0,0 @@
-dumpHTML has moved to the DumpHTML extension.
-
-WebDAV/SVN:
-http://svn.wikimedia.org/svnroot/mediawiki/trunk/extensions/DumpHTML/
-
-Web:
-http://svn.wikimedia.org/viewvc/mediawiki/trunk/extensions/DumpHTML/