diff options
| author | Regis-Gianas | 2014-10-30 22:13:21 +0100 |
|---|---|---|
| committer | Regis-Gianas | 2014-11-04 22:51:35 +0100 |
| commit | 812c611bdc8532b7cd25d9368a8356be3eb1d34a (patch) | |
| tree | 14c49e92d23052afcb4a802dd531d2bdf23f2118 /lib/xml_parser.mli | |
| parent | d21183a81fb73cd20ace5213cfe46c82250db38b (diff) | |
Xml_datatype.gxml: New type for semi-structured documents.
Xml_parser, Xml_printer: Use it.
Diffstat (limited to 'lib/xml_parser.mli')
0 files changed, 0 insertions, 0 deletions