1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 8e992cf4e3..d751682724 100644
--- a/Makefile
+++ b/Makefile
@@ -41,8 +41,8 @@ export MLFILES  := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml'  ')' $(FIN
 export MLIFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mli' ')' $(FIND_PRINTF_P)) \
   $(GENMLIFILES)
 export ML4FILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml4' ')' $(FIND_PRINTF_P))
-export VFILES   := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.v'   ')' $(FIND_PRINTF_P)) \
-  $(GENVFILES)
+#export VFILES   := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.v'   ')' $(FIND_PRINTF_P)) \
+#  $(GENVFILES)
 export CFILES   := $(shell find kernel/byterun -name '*.c')
 
 export ML4FILESML:= $(ML4FILES:.ml4=.ml)