aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/safe_typing.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-09-08 18:34:04 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-09-08 18:46:25 +0200
commit7cfe0a70eda671ada6a46cd779ef9308f7e0fdb9 (patch)
treeeeb9435bb4e64566647c5626a2a0f4b83eb58b08 /checker/safe_typing.ml
parent7a5eb53973ec3fd921b56339557c48681972849e (diff)
Removing the XML plugin.
Left a README, just in case someone will discover the remnants of it decades from now.
Diffstat (limited to 'checker/safe_typing.ml')
0 files changed, 0 insertions, 0 deletions