From bbc0922ad3c1206ed545c94579821d9b616f6cf1 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 30 May 2018 15:51:10 +0200
Subject: Makefile: fix undefined NATIVEFILES when -native-compute no

---
 Makefile.vofiles | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Makefile.vofiles b/Makefile.vofiles
index b1e97e9918..d0ae317335 100644
--- a/Makefile.vofiles
+++ b/Makefile.vofiles
@@ -32,6 +32,8 @@ vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst the
 GLOBFILES:=$(ALLVO:.vo=.glob)
 ifdef NATIVECOMPUTE
 NATIVEFILES := $(call vo_to_cm,$(ALLVO)) $(call vo_to_obj,$(ALLVO))
+else
+NATIVEFILES :=
 endif
 LIBFILES:=$(ALLVO) $(NATIVEFILES) $(VFILES) $(GLOBFILES)
 
-- 
cgit v1.2.3