From dffba98368b5b1156e1933dc7377317281c57491 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Fri, 9 Jun 2017 16:38:02 +0200
Subject: Makefile.common: remove an obsolete comment after PR#499

---
 Makefile.common | 2 --
 1 file changed, 2 deletions(-)

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index e7887f216a..62bbbc4fd7 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")) \
-- 
cgit v1.2.3