aboutsummaryrefslogtreecommitdiff
path: root/lib/xml_parser.ml
diff options
context:
space:
mode:
authorHugo Herbelin2014-11-03 20:16:48 +0100
committerHugo Herbelin2014-11-03 20:43:16 +0100
commitedbd6a211c934778d9721c36463836ef902b4fdd (patch)
tree0b7e03083914a80b52c862ddc0d945431d0b6d92 /lib/xml_parser.ml
parent9a6e94199b4df828f160e4a107debd7cb16e66bc (diff)
New bugs revealed fixed: #3408 by (probably) Maxime's commits
on vm and #3068 by Nov 2 commit on destruct. Also fixed test for failure of #3459.
Diffstat (limited to 'lib/xml_parser.ml')
0 files changed, 0 insertions, 0 deletions