summaryrefslogtreecommitdiff
path: root/src/urweb.grm
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2014-11-16 14:39:38 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2014-11-16 14:39:38 -0500
commitb24e1be86bca114f8a025c9b860e84e278044a5e (patch)
tree0d0ee3699880632ea91cb7e09112789d51bc1aa7 /src/urweb.grm
parent9d5548d15ef859eb57eb3b2124229bce9814a201 (diff)
Some more HTML5 input types
Diffstat (limited to 'src/urweb.grm')
-rw-r--r--src/urweb.grm1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/urweb.grm b/src/urweb.grm
index 85e5f092..5b568a8c 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -222,6 +222,7 @@ fun tagIn bt =
case bt of
"table" => "tabl"
| "url" => "url_"
+ | "datetime-local" => "datetime_local"
| _ => bt
datatype prop_kind = Delete | Update