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