> The first, making files in /usr/local/lib/mlton/include be writable by > the owner, is easy to do. It just uses the modes in the tar file. OK. Is it really the tar file or is it what happens when you install (see the install target in src/Makefile)? > As to the second, the new RPMs put them in /usr/share/doc, and I have decided > that that is fine. OK.