diff options
Diffstat (limited to 'src/fileio.sml')
| -rw-r--r-- | src/fileio.sml | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/src/fileio.sml b/src/fileio.sml index 72e72f6d..cab9d8a3 100644 --- a/src/fileio.sml +++ b/src/fileio.sml @@ -3,9 +3,14 @@ structure FileIO :> FILE_IO = struct val mostRecentModTimeRef = ref (Time.zeroTime) fun checkFileModTime fname = - let val mtime = OS.FileSys.modTime fname in - if Time.compare (mtime, !mostRecentModTimeRef) = GREATER andalso - Time.compare (mtime, Globals.getResetTime ()) = LESS + let + val mtime = OS.FileSys.modTime fname + val mostRecentMod = !mostRecentModTimeRef + val resetTime = Globals.getResetTime () + fun lessThan (a, b) = LargeInt.compare (Time.toSeconds a, Time.toSeconds b) = LESS + infix lessThan + in + if mostRecentMod lessThan mtime andalso mtime lessThan resetTime then mostRecentModTimeRef := mtime else () end |