aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-01-08 18:18:02 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-01-08 19:05:14 +0100
commitd08532d5344d96d10604760fa44109c9d56e73ce (patch)
tree2f5b472f526a6ad9f72cb57bde4503501f9c7129 /Makefile.common
parentb584c5529f7195849b0dd4f1eebf7c73c46f60db (diff)
Avoiding introducing yet another convention in naming files.
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common6
1 files changed, 3 insertions, 3 deletions
diff --git a/Makefile.common b/Makefile.common
index 7c98b64de..d752a5be9 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -68,7 +68,7 @@ CORESRCDIRS:=\
PLUGINS:=\
omega romega micromega quote \
setoid_ring extraction fourier \
- cc funind firstorder Derive \
+ cc funind firstorder derive \
rtauto nsatz syntax decl_mode btauto
SRCDIRS:=\
@@ -190,7 +190,7 @@ OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \
ascii_syntax_plugin.cma \
string_syntax_plugin.cma )
DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cma
-DERIVECMA:=plugins/Derive/derive_plugin.cma
+DERIVECMA:=plugins/derive/derive_plugin.cma
PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \
$(QUOTECMA) $(RINGCMA) \
@@ -314,7 +314,7 @@ BTAUTOVO:=$(call cat_vo_itarget, plugins/btauto)
RTAUTOVO:=$(call cat_vo_itarget, plugins/rtauto)
EXTRACTIONVO:=$(call cat_vo_itarget, plugins/extraction)
CCVO:=
-DERIVEVO:=$(call cat_vo_itarget, plugins/Derive)
+DERIVEVO:=$(call cat_vo_itarget, plugins/derive)
PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) \
$(FOURIERVO) $(CCVO) $(FUNINDVO) \