From 5ec51f923a11dbb3c38ceab4a1830e25a6449482 Mon Sep 17 00:00:00 2001
From: Gilles Peskine <Gilles.Peskine@arm.com>
Date: Tue, 10 Mar 2020 13:29:19 +0100
Subject: [PATCH] Future-proof `make clean` under Windows

In Windows cmd, `del foo` succeeds if `foo` doesn't exist, but
`del *.ext` fails if `*.ext` doesn't match any files. Therefore we use
the idiom `if exist *.ext del *.ext` to delete files matching
wildcards.

We've accidentally used `if exist $(some_list) del $(some_list)`, and
that's wrong, because it's only syntactically correct if
`$(some_list)` contains exactly one element. As long as `$(some_list)`
contains actual file names and not wildcards, just use `del $(some_list)`.
---
 programs/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/programs/Makefile b/programs/Makefile
index 9b2dcf022..deb19b6e3 100644
--- a/programs/Makefile
+++ b/programs/Makefile
@@ -363,7 +363,7 @@ ifndef WINDOWS
 else
 	if exist *.o del /Q /F *.o
 	if exist *.exe del /Q /F *.exe
-	if exist $(EXTRA_GENERATED) del /S /Q /F $(EXTRA_GENERATED)
+	del /S /Q /F $(EXTRA_GENERATED)
 endif
 	$(MAKE) -C fuzz clean