aboutsummaryrefslogtreecommitdiff
path: root/lib/xml_printer.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2015-07-29 12:12:35 +0200
committerPierre-Marie Pédrot2015-07-29 12:12:35 +0200
commite76ab0ec81040cbe99f616e8457bdc26cc6dceb6 (patch)
tree5bcdbed2dac27feeb27caf840e8cad24e7483a9a /lib/xml_printer.ml
parentaff5a1aaeb9b50c60ff32b7d5336a44fd18428ee (diff)
parent0dac9618c695a345f82ee302b205217fff29be29 (diff)
Merge branch 'v8.5'
Diffstat (limited to 'lib/xml_printer.ml')
-rw-r--r--lib/xml_printer.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/xml_printer.ml b/lib/xml_printer.ml
index eeddd53cb8..bbb7b51ba3 100644
--- a/lib/xml_printer.ml
+++ b/lib/xml_printer.ml
@@ -46,6 +46,8 @@ let buffer_attr tmp (n,v) =
match v.[p] with
| '\\' -> output "\\\\"
| '"' -> output "\\\""
+ | '<' -> output "&lt;"
+ | '&' -> output "&amp;"
| c -> output' c
done;
output' '"'