summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/fileio.sml11
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