rpm changes

[Stephen Weeks]

Henry, there are two changes that you in the past proposed making to the rpms
that I have not yet gotten around to.

1. Make files in /usr/local/lib/mlton/include writable.

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.

Please tell me if you still want both of these changes, and if so, what to do
about them.  Thanks.