diff options
| author | Regis-Gianas | 2014-10-30 18:09:09 +0100 |
|---|---|---|
| committer | Regis-Gianas | 2014-11-04 22:51:35 +0100 |
| commit | 7f40ab12d4ff5ecceccbeb72555e7c4421bd9dd0 (patch) | |
| tree | 83b819b82ed0d4b2b940ad7c30c5544eea15bfc8 /lib/xml_parser.ml | |
| parent | 1b25d0d5e710b65fdde7707bcf4ab926f4e65a87 (diff) | |
lib/Pp.ppcmd_token:
Extend this type with Ppcmd_open_tag and Ppcmd_close_tag.
lib/Pp.ppcmd_pp_dirs:
Handle these tags with a straightforward translation to
corresponding Format commands.
Diffstat (limited to 'lib/xml_parser.ml')
0 files changed, 0 insertions, 0 deletions