summaryrefslogtreecommitdiff
path: root/src/settings.sig
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2010-12-11 15:16:04 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2010-12-11 15:16:04 -0500
commitf327681cc734f2b478051f0174ca9d980ff2e5ae (patch)
tree83876d7a5e776b30240a4894ea70dfa58ddf120b /src/settings.sig
parent019d9a9c56bab7876983b78613e621d884ec20ae (diff)
minHeap option in .urp files
Diffstat (limited to 'src/settings.sig')
-rw-r--r--src/settings.sig3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/settings.sig b/src/settings.sig
index b72d007b..efbbdb32 100644
--- a/src/settings.sig
+++ b/src/settings.sig
@@ -211,4 +211,7 @@ signature SETTINGS = sig
val addLimit : string * int -> unit
val limits : unit -> (string * int) list
+
+ val setMinHeap : int -> unit
+ val getMinHeap : unit -> int
end