diff options
| -rw-r--r-- | Makefile.common | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/Makefile.common b/Makefile.common index e7887f216..62bbbc4fd 100644 --- a/Makefile.common +++ b/Makefile.common @@ -145,8 +145,6 @@ LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cmo=.cmx) # vo files ########################################################################### -## we now retrieve the names of .vo file to compile in */vo.itarget files - GENVOFILES := $(GENVFILES:.v=.vo) THEORIESVO := $(patsubst %.v,%.vo,$(shell find theories -type f -name "*.v")) \ |