aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/fileio.sig
diff options
context:
space:
mode:
authorGravatar Jacob Mitchell <jmitchell@member.fsf.org>2016-09-07 13:19:13 -0700
committerGravatar Jacob Mitchell <jmitchell@member.fsf.org>2016-09-07 13:19:13 -0700
commit51ac19f565fa935eec6d9dd1f7119c6227383a3c (patch)
tree9539e4a61dd38f2e65d78a5805b3eadef26cfebf /src/fileio.sig
parentc49ad46cc190e63f2395fcef03deff4386845877 (diff)
HTTP Last-Modified: latest modtime of source files
See issue #38.
Diffstat (limited to 'src/fileio.sig')
-rw-r--r--src/fileio.sig9
1 files changed, 9 insertions, 0 deletions
diff --git a/src/fileio.sig b/src/fileio.sig
new file mode 100644
index 00000000..37b3b529
--- /dev/null
+++ b/src/fileio.sig
@@ -0,0 +1,9 @@
+signature FILE_IO = sig
+
+ (* When was a source file last modified (excluding files produced after [getResetTime])? *)
+ val mostRecentModTime : unit -> Time.time
+
+ val txtOpenIn : string -> TextIO.instream
+ val binOpenIn : string -> BinIO.instream
+
+end