summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Vladimir Shabanov <vshabanoff@gmail.com>2012-09-04 03:32:59 +0400
committerGravatar Vladimir Shabanov <vshabanoff@gmail.com>2012-09-04 03:32:59 +0400
commit920ae25be5cdc22c8228aaa798149dc0301a93fa (patch)
tree10e35d56527ae19914997f754f6981fddeeab4f1
parent81e1fd6e36aec4af5749ac06004a55ad4c9b6bc6 (diff)
Added 'coreInline' and 'monoInline' .urp options
-rw-r--r--src/compiler.sml8
1 files changed, 8 insertions, 0 deletions
diff --git a/src/compiler.sml b/src/compiler.sml
index d1d0484a..603dd298 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -853,6 +853,14 @@ fun parseUrp' accLibs fname =
(case Int.fromString arg of
NONE => ErrorMsg.error ("invalid min heap '" ^ arg ^ "'")
| SOME n => minHeap := n)
+ | "coreInline" =>
+ (case Int.fromString arg of
+ NONE => ErrorMsg.error ("invalid core inline level '" ^ arg ^ "'")
+ | SOME n => Settings.setCoreInline n)
+ | "monoInline" =>
+ (case Int.fromString arg of
+ NONE => ErrorMsg.error ("invalid mono inline level '" ^ arg ^ "'")
+ | SOME n => Settings.setMonoInline n)
| "alwaysInline" => Settings.addAlwaysInline arg
| "noXsrfProtection" => Settings.addNoXsrfProtection arg
| "timeFormat" => Settings.setTimeFormat arg