summaryrefslogtreecommitdiff
path: root/src/urweb.grm
diff options
context:
space:
mode:
Diffstat (limited to 'src/urweb.grm')
-rw-r--r--src/urweb.grm9
1 files changed, 7 insertions, 2 deletions
diff --git a/src/urweb.grm b/src/urweb.grm
index 7a4d143f..db99d3b5 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -1397,6 +1397,11 @@ xmlOne : NOTAGS (EApp ((EVar (["Basis"], "cdata", Infer)
end)
| tag GT xmlOpt END_TAG (let
+ fun tagOut s =
+ case s of
+ "tabl" => "table"
+ | _ => s
+
val pos = s (tagleft, GTright)
val et = tagIn END_TAG
in
@@ -1423,9 +1428,9 @@ xmlOne : NOTAGS (EApp ((EVar (["Basis"], "cdata", Infer)
()
else
ErrorMsg.errorAt pos ("Begin tag <"
- ^ #1 (#1 tag)
+ ^ tagOut (#1 (#1 tag))
^ "> and end tag </"
- ^ et
+ ^ tagOut et
^ "> don't match.");
(EWild, pos))
end)