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