Mercurial > urweb
diff src/compiler.sml @ 1819:c9c38157d0d3
Merge
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Fri, 14 Sep 2012 06:44:14 -0400 |
parents | 28986cfac833 |
children | 8bc16ff91d32 |
line wrap: on
line diff
--- a/src/compiler.sml Wed Sep 12 19:49:02 2012 +0400 +++ b/src/compiler.sml Fri Sep 14 06:44:14 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