diff options
author | 2010-12-11 15:16:04 -0500 | |
---|---|---|
committer | 2010-12-11 15:16:04 -0500 | |
commit | 718af1b286a8fbd3f9f97358ab3bd995684f9543 (patch) | |
tree | 83876d7a5e776b30240a4894ea70dfa58ddf120b /src/settings.sml | |
parent | b30701c28e5a4072bc7efecc739fef12d509abc0 (diff) |
minHeap option in .urp files
Diffstat (limited to 'src/settings.sml')
-rw-r--r-- | src/settings.sml | 4 |
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 |