aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/settings.sml
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.sml
parent019d9a9c56bab7876983b78613e621d884ec20ae (diff)
minHeap option in .urp files
Diffstat (limited to 'src/settings.sml')
-rw-r--r--src/settings.sml4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/settings.sml b/src/settings.sml
index 7a943217..898b503f 100644
--- a/src/settings.sml
+++ b/src/settings.sml
@@ -509,4 +509,8 @@ fun addLimit (v as (name, _)) =
raise Fail ("Unknown limit category '" ^ name ^ "'")
fun limits () = !limitsList
+val minHeap = ref 0
+fun setMinHeap n = if n >= 0 then minHeap := n else raise Fail "Trying to set negative minHeap"
+fun getMinHeap () = !minHeap
+
end