summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-07-18 12:28:25 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-07-18 12:28:25 -0400
commitfb6f07a90bc6702d824fae8996c754341a3231b7 (patch)
tree11c610cfa009abe0f8e56ea72cae7e933da671b4
parent214006033ff59fb347593d91626924e3bab471a2 (diff)
Goodbye <font>; hello <h5> and <h6>
-rw-r--r--lib/ur/basis.urs3
1 files changed, 2 insertions, 1 deletions
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index d0a8af06..c4520ae7 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -569,12 +569,13 @@ val p : bodyTag boxEvents
val b : bodyTag boxEvents
val i : bodyTag boxEvents
val tt : bodyTag boxEvents
-val font : bodyTag ([Size = int, Face = string] ++ boxEvents)
val h1 : bodyTag boxEvents
val h2 : bodyTag boxEvents
val h3 : bodyTag boxEvents
val h4 : bodyTag boxEvents
+val h5 : bodyTag boxEvents
+val h6 : bodyTag boxEvents
val li : bodyTag boxEvents
val ol : bodyTag boxEvents