diff options
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. ## |