tree babde1685b5270308089ec193ae79690b50e3632
parent a647f1296e927062c8a84486fd699558770aa934
author Gilles Peskine <Gilles.Peskine@arm.com> 1583843359 +0100
committer Gilles Peskine <Gilles.Peskine@arm.com> 1584982532 +0100

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)`.