Drop the compression helper

The kludge of pulling files from github no longer works now
that we have a build process, and since most people have their
own build pipeline now, I don't feel that supporting on-website
builds is that important anymore.

Author: marijnh

bin/release

@@ -32,11 +32,6 @@ if (bumpOnly) process.exit(0);
 
 child.exec("bash bin/authors.sh", function(){});
 
-rewrite("doc/compress.html", function(cmp) {
-  return cmp.replace(/<option value="http:\/\/codemirror.net\/">HEAD<\/option>/,
-                     "<option value=\"http://codemirror.net/\">HEAD</option>\n        <option value=\"http://marijnhaverbeke.nl/git/codemirror?a=blob_plain;hb=" + number + ";f=\">" + number + "</option>");
-});
-
 rewrite("index.html", function(index) {
   return index.replace(/\.zip">\d+\.\d+\.\d+<\/a>/,
                        ".zip\">" + number + "</a>");