]> git.ipfire.org Git - thirdparty/make.git/commitdiff
* maintMakefile: Don't make .check-git-HEAD .PHONY
authorPaul Smith <psmith@gnu.org>
Sun, 14 Mar 2021 19:53:45 +0000 (15:53 -0400)
committerPaul Smith <psmith@gnu.org>
Sun, 14 Mar 2021 19:53:45 +0000 (15:53 -0400)
maintMakefile

index 490679876dc2b2fb56557dcc3af0dc42144a40fd..e3edd0a0e4998157293d5255090247d8cd7b9567 100644 (file)
@@ -137,12 +137,13 @@ ChangeLog: .check-git-HEAD
            echo "WARNING: $(gl2cl) is not available.  No $@ generated."; \
        fi
 
-.PHONY: .check-git-HEAD
-.check-git-HEAD:
+.check-git-HEAD: FORCE
        sha="`git rev-parse HEAD`"; \
        test -f '$@' && [ "`cat '$@' 2>/dev/null`" = "$$sha" ] \
            || echo "$$sha" > '$@'
 
+.PHONY: FORCE
+FORCE:;@:
 
 ## ---------------- ##
 ## Updating files.  ##