diff options
Diffstat (limited to 'lib/Support/Makefile')
| -rw-r--r-- | lib/Support/Makefile | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/lib/Support/Makefile b/lib/Support/Makefile index 67272908..ff28b06e 100644 --- a/lib/Support/Makefile +++ b/lib/Support/Makefile @@ -14,4 +14,23 @@ DONT_BUILD_RELINKED=1 BUILD_ARCHIVE=1 NO_INSTALL=1 +# FIXME: This is nasty. We don't want to rebuild this library everytime +# but this was the only way I could find to make the build work. +# +# Note this rule has to go here so it is run first. +CompileTimeInfoFile:=../../include/klee/Config/CompileTimeInfo.h +all-local:: $(CompileTimeInfoFile) + include $(LEVEL)/Makefile.common + + +GIT_PRESENT:=$(shell [ -d "$(PROJ_SRC_ROOT)/.git" ] && echo 1 || echo 0) + +.PHONY: $(CompileTimeInfoFile) +$(CompileTimeInfoFile): + $(Verb) echo "Regenerating $(CompileTimeInfoFile)" + $(Verb) echo '#define KLEE_BUILD_MODE "$(BuildMode)"' > $(CompileTimeInfoFile) +ifeq ($(GIT_PRESENT),1) + $(Verb) echo '#define KLEE_BUILD_REVISION "'$(shell cd $(PROJ_SRC_ROOT); git rev-parse HEAD)'"' >> \ + $(CompileTimeInfoFile) +endif |