aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--Makefile.common2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common
index 6dc193d6e..b47a3e322 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -67,7 +67,7 @@ CORESRCDIRS:=\
PLUGINS:=\
omega romega micromega quote \
- setoid_ring xml extraction fourier \
+ setoid_ring extraction fourier \
cc funind firstorder Derive \
rtauto nsatz syntax decl_mode btauto