[MLton] web update

[Stephen Weeks]

> I made a minor change to index.html in the mlton/web repository, but I
> don't know how to push it out to the web.

The web lives on mlton.org in

	/var/www/html/mlton.org/

I've gone ahead and pushed the new home page.  I guess it would be
nice to have a script that runs on mlton.org and syncs up the web with
the CVS.

> (The change was a Google box next to each of the mailing lists that has
> enough site: and inurl: options to effectively search just the appropriate
> archives.  

Neat!  What do you think about changing the button name to "Search" or
"Search Archives"?

> I wouldn't mind moving the boxes to the appropriate archive pages, but it
> seemed to me that those pages were automatically generated, and, in any
> case, they weren't in the repository.

The listinfo pages, like

	http://www.mlton.org/mailman/listinfo/mlton

are edited at

	http://www.mlton.org/mailman/admin/mlton

which I believe runs scripts that change

	/var/mailman/lists/mlton/config.db

The archive pages, like

	http://www.mlton.org/pipermail/mlton/

are autogenerated by

	/var/mailman/Mailman/Archiver/HyperArch.py

I did a small change of that file at some point to disable the ability
to download the entire archive.  You could edit that file to add a
search button to the top of the archive pages.  That would be nice.
But I wouldn't take the buttons away from the mlton.org home page --
they're useful there too.

On a mildly related note, it would be a really nice project to rewrite
Mailman in MLton -- it would run a lot faster.  It was really painful
when I had to build the initial archives from all our old messages.

Also, Matthew, feel free to change your affiliation on the team.html
page now that you've moved on to Harvard.