summaryrefslogtreecommitdiff
path: root/src/globals.sig
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@mit.edu>2016-10-23 14:26:59 -0400
committerGravatar Benjamin Barenblat <bbaren@mit.edu>2016-10-23 14:26:59 -0400
commit235602373c04aa38b7f8c93e6efbd9276ecc2266 (patch)
tree97c39e67902dd84d088ab930d8675e90760a674a /src/globals.sig
parentc921d0df325c803fed8c7742eb088cb3d030d541 (diff)
parent20f3308b8c2a5a331239839e222bd21befde73eb (diff)
Merge branch 'upstream' into dfsg_clean20161022+dfsg
Diffstat (limited to 'src/globals.sig')
-rw-r--r--src/globals.sig7
1 files changed, 7 insertions, 0 deletions
diff --git a/src/globals.sig b/src/globals.sig
new file mode 100644
index 00000000..0cff65b5
--- /dev/null
+++ b/src/globals.sig
@@ -0,0 +1,7 @@
+signature GLOBALS = sig
+
+ (* When was the Ur/Web compiler started or reset? *)
+ val setResetTime : unit -> unit
+ val getResetTime : unit -> Time.time
+
+end