From: Lady <redacted>
Date: Fri, 24 May 2024 05:10:58 +0000 (-0400)
Subject: Mark GNUmakefile as precious
X-Git-Tag: 0.9.3~3
X-Git-Url: https://git.ladys.computer/Shushe/commitdiff_plain/c5203f114453b0baf387c86071367e3c29ce1a0c?hp=3339490e52d47775af7ec4a5d2e7b683ec9541b1

Mark GNUmakefile as precious

One would hope that Make wouldn’t ever delete the make·file it is
running, but the documentation doesn’t seem to explicitly give that
guarantee, so it’s good to be explicit about it.
---

diff --git a/GNUmakefile b/GNUmakefile
index d54df18..46fb27d 100644
--- a/GNUmakefile
+++ b/GNUmakefile
@@ -538,6 +538,9 @@ FORCE : ;
 # Don’t use any implicit rules.
 .SUFFIXES : ;
 
+# Don’t delete these files even if Make is stopped in the process of rebuilding them.
+.PRECIOUS : GNUmakefile ;
+
 # Phony rules; always consider these out·of·date.
 .PHONY : FORCE all default clean gone info install list listout uninstall $(call built,$(recursivefiles)) ;