From 53d30eb8b3186031658dafd74dc7ad012854f385 Mon Sep 17 00:00:00 2001
From: Vadim Zaliva <lord@crocodile.org>
Date: Wed, 8 Mar 2017 23:05:55 -0800
Subject: Fix #5132: coq_makefile generates incorrect install goal

---
 tools/coq_makefile.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'tools')

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index b7dd5f2a1..294575e0a 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -676,6 +676,7 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
       print "VO=vo\n";
       print "VOFILES:=$(VFILES:.v=.$(VO))\n";
       classify_files_by_root "VOFILES" l inc;
+      classify_files_by_root "VFILES" l inc;
       print "GLOBFILES:=$(VFILES:.v=.glob)\n";
       print "GFILES:=$(VFILES:.v=.g)\n";
       print "HTMLFILES:=$(VFILES:.v=.html)\n";
-- 
cgit v1.2.3