aboutsummaryrefslogtreecommitdiff
path: root/contrib/xml
ModeNameSize
-rw-r--r--COPYRIGHT592logplain
-rw-r--r--README5663logplain
-rw-r--r--Xml.v1760logplain
-rw-r--r--xml.ml3164logplain
-rw-r--r--xml.mli2224logplain
-rw-r--r--xmlcommand.ml37026logplain
-rw-r--r--xmlcommand.mli3239logplain
-rw-r--r--xmlentries.ml2184logplain