diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-06-09 16:38:02 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-06-09 16:38:02 +0200 |
| commit | dffba98368b5b1156e1933dc7377317281c57491 (patch) | |
| tree | e2716a2e3a965e2009e805927d71e38185fd811d /Makefile.common | |
| parent | 3e1f527a50142a5c73ead24e3fcdb6e2ac9f50e5 (diff) | |
Makefile.common: remove an obsolete comment after PR#499
Diffstat (limited to 'Makefile.common')
| -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")) \ |