[MLton] web update

Matthew Fluet fluet@cs.cornell.edu
Mon, 31 May 2004 09:06:57 -0400 (EDT)


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 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.  Much faster and more convenient than grep on a mailbox file.
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.)