Mercurial > urweb
comparison src/compiler.sml @ 1629:438561303d02
timeFormat .urp directive
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sun, 04 Dec 2011 14:40:12 -0500 |
parents | f4453e2402d0 |
children | e374b6b8ab38 |
comparison
equal
deleted
inserted
replaced
1628:3621f486ce72 | 1629:438561303d02 |
---|---|
797 (case Int.fromString arg of | 797 (case Int.fromString arg of |
798 NONE => ErrorMsg.error ("invalid min heap '" ^ arg ^ "'") | 798 NONE => ErrorMsg.error ("invalid min heap '" ^ arg ^ "'") |
799 | SOME n => minHeap := n) | 799 | SOME n => minHeap := n) |
800 | "alwaysInline" => Settings.addAlwaysInline arg | 800 | "alwaysInline" => Settings.addAlwaysInline arg |
801 | "noXsrfProtection" => Settings.addNoXsrfProtection arg | 801 | "noXsrfProtection" => Settings.addNoXsrfProtection arg |
802 | "timeFormat" => Settings.setTimeFormat arg | |
802 | 803 |
803 | _ => ErrorMsg.error ("Unrecognized command '" ^ cmd ^ "'"); | 804 | _ => ErrorMsg.error ("Unrecognized command '" ^ cmd ^ "'"); |
804 read () | 805 read () |
805 end | 806 end |
806 | 807 |