diff options
| author | Scott Gasch <[email protected]> | 2026-10-05 10:43:26 -0700 |
|---|---|---|
| committer | Scott Gasch <[email protected]> | 2026-10-05 10:43:26 -0700 |
| commit | e5c845d7e0b936641158909dbc516a79958c74e8 (patch) | |
| tree | eaa8113b67d21ecea04a2dbae860c7fe0e3b10cd /src/GNUmakefile | |
| parent | 64b5d3307a7a95975f7f8c0248f3f1febedd8617 (diff) | |
Update makefile and logfile to work with linux.
Diffstat (limited to 'src/GNUmakefile')
| -rw-r--r-- | src/GNUmakefile | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/GNUmakefile b/src/GNUmakefile index b9b6d16..eb7eb2d 100644 --- a/src/GNUmakefile +++ b/src/GNUmakefile @@ -285,7 +285,10 @@ endif # the PROFILE-overwriting `=` assignments above (not `+=`), so it # survives into CFLAGS instead of being wiped out by them. GIT_COMMIT := $(shell git rev-parse --short HEAD 2>/dev/null || echo unknown) -GIT_DIRTY := $(shell git diff --quiet 2>/dev/null || echo -dirty) +# Scoped to this directory: an unscoped `git diff` has to stat (and, +# with a stale index, re-hash) every tracked file in the repo, +# including the multi-GB pgn/twic.pgn, on every make invocation. +GIT_DIRTY := $(shell git diff --quiet -- . 2>/dev/null || echo -dirty) # Kept out of PROFILE itself (not folded in via +=): PROFILE gets # stringified whole into -DPROFILE="..." below for the "Make profile # used" trace line, and this value's embedded quotes broke that outer |