aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/pluginsopt.itarget
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 /plugins/pluginsopt.itarget
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 'plugins/pluginsopt.itarget')
-rw-r--r--plugins/pluginsopt.itarget1
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/pluginsopt.itarget b/plugins/pluginsopt.itarget
index 34b024663..e44d7c149 100644
--- a/plugins/pluginsopt.itarget
+++ b/plugins/pluginsopt.itarget
@@ -8,7 +8,6 @@ fourier/fourier_plugin.cmxa
romega/romega_plugin.cmxa
omega/omega_plugin.cmxa
micromega/micromega_plugin.cmxa
-xml/xml_plugin.cmxa
cc/cc_plugin.cmxa
nsatz/nsatz_plugin.cmxa
funind/recdef_plugin.cmxa