1 files changed, 23 insertions, 0 deletions
diff --git a/plugins/pluginsopt.itarget b/plugins/pluginsopt.itarget
new file mode 100644
index 00000000..2f72dab8
--- /dev/null
+++ b/plugins/pluginsopt.itarget
@@ -0,0 +1,23 @@
+field/field_plugin.cmxa
+setoid_ring/newring_plugin.cmxa
+extraction/extraction_plugin.cmxa
+firstorder/ground_plugin.cmxa
+rtauto/rtauto_plugin.cmxa
+fourier/fourier_plugin.cmxa
+romega/romega_plugin.cmxa
+omega/omega_plugin.cmxa
+micromega/micromega_plugin.cmxa
+dp/dp_plugin.cmxa
+xml/xml_plugin.cmxa
+subtac/subtac_plugin.cmxa
+ring/ring_plugin.cmxa
+cc/cc_plugin.cmxa
+nsatz/nsatz_plugin.cmxa
+funind/recdef_plugin.cmxa
+syntax/ascii_syntax_plugin.cmxa
+syntax/nat_syntax_plugin.cmxa
+syntax/numbers_syntax_plugin.cmxa
+syntax/r_syntax_plugin.cmxa
+syntax/string_syntax_plugin.cmxa
+syntax/z_syntax_plugin.cmxa
+quote/quote_plugin.cmxa