Skip to content

Commit 7b4b8fe

Browse files
committed
Make's file function is only available from 4.2 onwards
Just removing this optimisation as it is only a fraction of the cost of the git invocation.
1 parent ca982a5 commit 7b4b8fe

File tree

1 file changed

+0
-6
lines changed

1 file changed

+0
-6
lines changed

src/common

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -239,13 +239,7 @@ else
239239
$(CBMC_VERSION_FILES): CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
240240
endif
241241

242-
# Use make >= 4.0's `file` function, if available - it should be faster than
243-
# `shell cat`
244-
ifeq ($(firstword $(subst ., , $(MAKE_VERSION))), 3)
245242
KNOWN_RELEASE_INFO = $(shell cat $(GIT_INFO_FILE) 2>/dev/null)
246-
else
247-
KNOWN_RELEASE_INFO = $(file < $(GIT_INFO_FILE))
248-
endif
249243
ifneq ($(GIT_INFO), $(KNOWN_RELEASE_INFO))
250244
$(CBMC_VERSION_FILES): $(GIT_INFO_FILE)
251245

0 commit comments

Comments
 (0)