I don't if this was there before, but in the binary RPM, the stuff that gets put in /usr/local/lib/mlton/include is mode 666 (writable by everyone). It should be 644 (although 444 would not be horrible). This is VERY BAD.