[MLton-user] Thanks !

Stephen Weeks MLton-user@mlton.org
Thu, 8 Dec 2005 08:29:21 -0800


> Perhaps moving things from /usr/* to /* for the cygwin port would
> be a good idea. That way it would work even for windows tools.

I'm OK with moving /usr/{bin,lib} to /{bin,lib}, but I think we should
leave the docs in /usr/share/doc/mlton, not move them to
/share/doc/mlton.