diff src/urweb.grm @ 2077:3cd2bd4b1de0

More simple textual HTML5 input types
author Adam Chlipala <adam@chlipala.net>
date Sun, 16 Nov 2014 14:16:11 -0500
parents fde864eacd47
children 6d126af2e1cb
line wrap: on
line diff
--- a/src/urweb.grm	Sun Nov 16 14:06:24 2014 -0500
+++ b/src/urweb.grm	Sun Nov 16 14:16:11 2014 -0500
@@ -221,6 +221,7 @@
 fun tagIn bt =
     case bt of
         "table" => "tabl"
+      | "url" => "url_"
       | _ => bt
 
 datatype prop_kind = Delete | Update