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?ds=inline

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)) ;