rpm changes

Stephen Weeks MLton@sourcelight.com
Fri, 22 Jun 2001 11:52:48 -0700


> 2. The current RPM is installing everything in /usr/local EXCEPT for the doc
>    stuff which it puts in /usr/doc.  Not anthing horrible, but really not
>    the right place.  Something I should probably fix in the future.

I now notice that the new rpms on red hat 7.1 put the docs in 
/usr/share/doc/mlton-...

Maybe that is good enough?