diff options
author | Paul Smith <psmith@gnu.org> | 2021-03-14 15:53:45 -0400 |
---|---|---|
committer | Paul Smith <psmith@gnu.org> | 2021-03-14 15:53:45 -0400 |
commit | d9aff6b81731ba55a502d3768a55233b666877fd (patch) | |
tree | 0d7a15b05f6ceef88761991087997a08069d3ccf | |
parent | e5f6dc54b9d1454cd3d3a2152ff73802c7c4b2b0 (diff) | |
download | make-git-d9aff6b81731ba55a502d3768a55233b666877fd.tar.gz |
* maintMakefile: Don't make .check-git-HEAD .PHONY
-rw-r--r-- | maintMakefile | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/maintMakefile b/maintMakefile index 49067987..e3edd0a0 100644 --- a/maintMakefile +++ b/maintMakefile @@ -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. ## |