summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-03-20 18:46:45 -0400
committerMorgan Deters <mdeters@cs.nyu.edu>2013-03-20 20:00:55 -0400
commita8df78d4ce070fea927075eeb7e6d283f8e64e34 (patch)
treecd7484598d6ecd044d590ea1d4caacab43760a55 /src/util
parentb480438b3d39000cfac88eac12922a23f9fccbea (diff)
Better reporting of detached git state in --version and --show-config
Diffstat (limited to 'src/util')
-rw-r--r--src/util/configuration.cpp7
1 files changed, 6 insertions, 1 deletions
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();
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback