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 d54df18083999ba74d71e316be4c10b21013cd28..46fb27dc62c8e2ac2e7ab72914749b6c460974a0 100644 (file)
--- a/GNUmakefile
+++ b/GNUmakefile
@@ -538,6 +538,9 @@ FORCE : ;
 # Don’t use any implicit rules.
 .SUFFIXES : ;
 
 # 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)) ;
 
 # Phony rules; always consider these out·of·date.
 .PHONY : FORCE all default clean gone info install list listout uninstall $(call built,$(recursivefiles)) ;