aboutsummaryrefslogtreecommitdiff
path: root/plugins/xml/xmlcommand.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2013-12-01 18:47:55 +0100
committerPierre-Marie Pédrot2013-12-01 18:55:11 +0100
commitcb290d81c46ec370e303e1414e203c40c8fa1174 (patch)
tree8f48d26fe7f68a905c2194239523c91316dc0139 /plugins/xml/xmlcommand.ml
parent233a782a2336f003869f82e697a567ed02885f23 (diff)
Removing RefArgType generic argument.
Diffstat (limited to 'plugins/xml/xmlcommand.ml')
0 files changed, 0 insertions, 0 deletions