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 /maintMakefile | |
| parent | e5f6dc54b9d1454cd3d3a2152ff73802c7c4b2b0 (diff) | |
| download | make-git-d9aff6b81731ba55a502d3768a55233b666877fd.tar.gz | |
* maintMakefile: Don't make .check-git-HEAD .PHONY
Diffstat (limited to 'maintMakefile')
| -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. ## |