diff options
| author |  Adam Chlipala <adamc@csail.mit.edu> | 2016-09-20 13:46:57 -0400 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2016-09-20 13:46:57 -0400 |
| commit | d41ec985e9839d5c01d69363cfca1dfda25536ab (patch) | |
| tree | c32d4e40b99242c7eba2ae198639611753425240 | |
| parent | 3afe16344c02881e4ace9e8965f48154b5225638 (diff) | |
| parent | 2f81ca80930450cbbb12dba7abd112e7b296f1f6 (diff) | |
Merge pull request #51 from jmitchell/bin-repro-mtime-precision
Use 1s precision when comparing file mtimes
| -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 |