[MLton] web update

[Matthew Fluet]

> > 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.

That's what I thought, but the fact that sufficient numbers of files and
directories didn't match up between the repository and
/var/www/html/mlton.org made me suspicious.  And I didn't know where on
mlton.org I should copy the files from.

> > (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"?

"Search Archive" would be fine.

> 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.

That seems to be a little harder, since HyperArch.py is generating archive
pages for arbitrary lists.  Note that in order to narrow google enough,
when you search the  mlton  list, then I pass  -inurl:user  to filter out
the  mlton-user  list, while to search the  mlton-user  list, I pass
+inulr:user  to filter the other way.

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

Well, my affiliation remains Cornell; I'm just physically located at
Harvard.