# HG changeset patch # User Vladimir Shabanov # Date 1346715179 -14400 # Node ID 28986cfac833cdaa13f9073d79e141b506f38c1d # Parent 2d9f831d45c90334c54bc810bdcbd11b852a76f5 Added 'coreInline' and 'monoInline' .urp options diff -r 2d9f831d45c9 -r 28986cfac833 src/compiler.sml --- a/src/compiler.sml Mon Sep 03 09:51:23 2012 -0400 +++ b/src/compiler.sml Tue Sep 04 03:32:59 2012 +0400 @@ -853,6 +853,14 @@ (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