From 47a5805434c2cc9f1d705bd3327728e2b9cae6ba Mon Sep 17 00:00:00 2001
From: Francisco Molina <femolina@uc.cl>
Date: Thu, 28 May 2020 10:09:36 +0200
Subject: [PATCH] Makefile: add BINFILE to default BUILD_FILES

---
 Makefile.include | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/Makefile.include b/Makefile.include
index 8dd0ae1584..11135a0cd8 100644
--- a/Makefile.include
+++ b/Makefile.include
@@ -531,8 +531,13 @@ ifeq (,$(FLASHFILE))
   $(error FLASHFILE is not defined for this board: $(FLASHFILE))
 endif
 
-# By default always build ELFFILE and FLASHFILE
-BUILD_FILES += $(ELFFILE) $(FLASHFILE)
+# By default always build ELFFILE, BINFILE and FLASHFILE
+ifeq ($(RIOT_CI_BUILD),1)
+  # Don't build BINFILE on the CI to save some computation time
+  BUILD_FILES += $(ELFFILE) $(FLASHFILE)
+else
+  BUILD_FILES += $(ELFFILE) $(BINFILE) $(FLASHFILE)
+endif
 
 # variables used to compile and link c++
 CPPMIX ?= $(if $(wildcard *.cpp),1,)