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