star-build

commit 76cc978aaf360f8a07ead24d129948967d3ef570
parent f1c1089705ceb33835fcaa67b930fc0de29f0d5f
Author: Vincent Forest <vincent.forest@meso-star.com>
Date:   Mon, 16 Dec 2024 14:10:07 +0100

Rm the previously generated makefile before compilation

The file may have been generated by another user, such as root, if a
privilege escalation was used for compilation; for example, to install
in a directory to which the current user has no write access.

In this case, the file could not be updated, since it would belong to
another user, but could be deleted, since it can be assumed that the src
directory belongs to the current user, who presumably has read access to
the said makefile.

Diffstat:
M
Makefile
 | 
1
+

1 file changed, 1 insertion(+), 0 deletions(-)
diff --git a/Makefile b/Makefile
@@ -46,6 +46,7 @@ mirror: makefile
 # Generate the Makefile of the build
 makefile: cache
 	@echo "Setup $(MK)"
+	@rm -f $(MK)
 	@{ \
 	  PATH="src:$${PATH}" \
 	  USE_SIMD=$(USE_SIMD) \