[MLton] mlb support
Henry Cejtin
henry@sourcelight.com
Wed, 21 Jul 2004 23:01:40 -0500
Re inode changing and the like, why not just check them on startup each time.
I.e., stash away in the saved world, the device, inode and ctime. (The ctime
changes when you do any thing to the file except rename it. All ops change
the ctime to the current time and there is no way to set the ctime back.)
This way if files are changed in any way, the stamp would change. In cases
where a saved basis file turned out to be invalid on a run (because of these
having changed) you would issue a warning to stderr saying that the cache
should be re-built, and, for that run, read them in again.
Re short names, I agree that it isn't a big deal, but I find it annoying to
have to read stuff just to make sure that it is what it almost certainly is.
Any way, clearly not really important either way.