diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-20 18:46:45 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-20 20:00:55 -0400 |
| commit | a8df78d4ce070fea927075eeb7e6d283f8e64e34 (patch) | |
| tree | cd7484598d6ecd044d590ea1d4caacab43760a55 /src | |
| parent | b480438b3d39000cfac88eac12922a23f9fccbea (diff) | |
Better reporting of detached git state in --version and --show-config
Diffstat (limited to 'src')
| -rw-r--r-- | src/Makefile.am | 2 | ||||
| -rw-r--r-- | src/main/options_handlers.h | 6 | ||||
| -rw-r--r-- | src/util/configuration.cpp | 7 |
3 files changed, 12 insertions, 3 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 3d90f302e..b505750d4 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -137,7 +137,7 @@ gitinfo: gitinfo.tmp # .PHONY ensures the .tmp version is always rebuilt (to check for any changes) .PHONY: gitinfo.tmp gitinfo.tmp: - $(AM_V_GEN)(cd "$(top_srcdir)" && sed 's,^ref: refs/heads/,,' .git/HEAD && git show-ref refs/heads/`sed 's,^ref: refs/heads/,,' .git/HEAD` && echo "Modifications: `test -z \"\`git status -s -uno\`\" && echo false || echo true`") >"$@" 2>/dev/null || true + $(AM_V_GEN)(cd "$(top_srcdir)"; if ! grep -q '^ref: refs/heads/' .git/HEAD; then echo; fi; sed 's,^ref: refs/heads/,,' .git/HEAD; git show-ref refs/heads/`sed 's,^ref: refs/heads/,,' .git/HEAD`; echo "Modifications: `test -z \"\`git status -s -uno\`\" && echo false || echo true`") >"$@" 2>/dev/null || true install-data-local: (echo include/cvc4.h; \ diff --git a/src/main/options_handlers.h b/src/main/options_handlers.h index f14a67d5f..4bb4841fe 100644 --- a/src/main/options_handlers.h +++ b/src/main/options_handlers.h @@ -27,8 +27,12 @@ inline void showConfiguration(std::string option, SmtEngine* smt) { printf("\n"); printf("version : %s\n", Configuration::getVersionString().c_str()); if(Configuration::isGitBuild()) { + const char* branchName = Configuration::getGitBranchName(); + if(*branchName == '\0') { + branchName = "-"; + } printf("scm : git [%s %s%s]\n", - Configuration::getGitBranchName(), + branchName, std::string(Configuration::getGitCommit()).substr(0, 8).c_str(), Configuration::hasGitModifications() ? " (with modifications)" : ""); diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index 9be4e4104..ce6273a13 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -216,8 +216,13 @@ std::string Configuration::getGitId() { return ""; } + const char* branchName = getGitBranchName(); + if(*branchName == '\0') { + branchName = "-"; + } + stringstream ss; - ss << "git " << getGitBranchName() << " " << string(getGitCommit()).substr(0, 8) + ss << "git " << branchName << " " << string(getGitCommit()).substr(0, 8) << ( ::CVC4::Configuration::hasGitModifications() ? " (with modifications)" : "" ); return ss.str(); } |