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/main/options_handlers.h | |
| parent | b480438b3d39000cfac88eac12922a23f9fccbea (diff) | |
Better reporting of detached git state in --version and --show-config
Diffstat (limited to 'src/main/options_handlers.h')
| -rw-r--r-- | src/main/options_handlers.h | 6 |
1 files changed, 5 insertions, 1 deletions
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)" : ""); |