github-repos/make
1
0
Fork 0
mirror of https://github.com/mirror/make.git synced 2025-02-05 01:00:11 +08:00
Code Issues Packages Projects Releases Wiki Activity

* maintMakefile: Don't make .check-git-HEAD .PHONY

Browse Source
This commit is contained in:
Paul Smith 2021-03-14 15:53:45 -04:00
parent e5f6dc54b9
commit d9aff6b817
1 changed files with 3 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
maintMakefile
View File

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