summaryrefslogtreecommitdiff
path: root/stdlib/spacetime.mli
diff options
context:
space:
mode:
authorLeo White <lpw25@cl.cam.ac.uk>2016-10-11 10:54:09 +0100
committerLeo White <lpw25@cl.cam.ac.uk>2017-01-10 10:07:40 +0000
commit4ace3d0776c1225d6c714ed69b93ce6b221d64fd (patch)
treec1155572864b9cbd0e90399bb86a217f200019bb /stdlib/spacetime.mli
parent5ed72007f8185b2bd3c7a663abdcb1be5eaeee7c (diff)
downloadocaml-4ace3d0776c1225d6c714ed69b93ce6b221d64fd.tar.gz
Expose Spacetime.enabled
Diffstat (limited to 'stdlib/spacetime.mli')
-rw-r--r--stdlib/spacetime.mli4
1 files changed, 4 insertions, 0 deletions
diff --git a/stdlib/spacetime.mli b/stdlib/spacetime.mli
index 5f3b51e64d..eb8bd11a93 100644
--- a/stdlib/spacetime.mli
+++ b/stdlib/spacetime.mli
@@ -50,6 +50,10 @@
For functions to decode the information recorded by the profiler,
see the Spacetime offline library in otherlibs/. *)
+(** [enabled] is [true] if the compiler is configured with spacetime and [false]
+ otherwise *)
+val enabled : bool
+
module Series : sig
(** Type representing a file that will hold a series of heap snapshots
together with additional information required to interpret those