[MLton] web update
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 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
Neat! What do you think about changing the button name to "Search" or
> 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.