[MLton] web update

Stephen Weeks MLton@mlton.org
Mon, 31 May 2004 12:22:10 -0700

> 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


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


are edited at


which I believe runs scripts that change


The archive pages, like


are autogenerated by


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.