diff options
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/Makefile.common b/Makefile.common index d5f79d76b5..b936eb4c74 100644 --- a/Makefile.common +++ b/Makefile.common @@ -146,14 +146,16 @@ LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cmo=.cmx) ## we now retrieve the names of .vo file to compile in */vo.itarget files -THEORIESVO:= $(foreach f, $(wildcard theories/*/vo.itarget), \ - $(addprefix $(dir $(f)),$(shell cat $(f)))) +GENVOFILES := $(GENVFILES:.v=.vo) -PLUGINSVO:= $(foreach f, $(wildcard plugins/*/vo.itarget), \ - $(addprefix $(dir $(f)),$(shell cat $(f)))) +THEORIESVO := $(patsubst %.v,%.vo,$(shell find theories -type f -name "*.v")) \ + $(filter theories/%, $(GENVOFILES)) -ALLVO:= $(THEORIESVO) $(PLUGINSVO) -VFILES:= $(ALLVO:.vo=.v) +PLUGINSVO := $(patsubst %.v,%.vo,$(shell find plugins -type f -name "*.v")) \ + $(filter plugins/%, $(GENVOFILES)) + +ALLVO := $(THEORIESVO) $(PLUGINSVO) +VFILES := $(ALLVO:.vo=.v) ## More specific targets @@ -175,11 +177,10 @@ vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theo vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.o))))) -LIBFILES:=$(THEORIESVO) $(PLUGINSVO) $(call vo_to_cm,$(THEORIESVO)) \ - $(call vo_to_cm,$(PLUGINSVO)) $(call vo_to_obj,$(THEORIESVO)) \ - $(call vo_to_obj,$(PLUGINSVO)) \ - $(PLUGINSVO:.vo=.v) $(THEORIESVO:.vo=.v) \ - $(PLUGINSVO:.vo=.glob) $(THEORIESVO:.vo=.glob) +GLOBFILES:=$(ALLVO:.vo=.glob) +LIBFILES:=$(ALLVO) $(call vo_to_cm,$(ALLVO)) \ + $(call vo_to_obj,$(ALLVO)) \ + $(VFILES) $(GLOBFILES) # For emacs: # Local Variables: |