From 97b33cf8b19e1f08f318fef47192fe4cde3971f0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 11 Mar 2017 08:39:25 +0100 Subject: [PATCH] changed version output slightly --- src/storm/utility/storm-version.h | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/storm/utility/storm-version.h b/src/storm/utility/storm-version.h index 24cf9a36f..cfe705304 100644 --- a/src/storm/utility/storm-version.h +++ b/src/storm/utility/storm-version.h @@ -24,7 +24,7 @@ namespace storm { /// How many commits passed since the tag was last set. const static unsigned commitsAhead; - /// 0 iff there no files were modified in the checkout, 1 otherwise. + /// 0 iff there no files were modified in the checkout, 1 otherwise. If none, no information about dirtyness is given. const static boost::optional dirty; /// The system which has compiled Storm. @@ -53,6 +53,8 @@ namespace storm { } if (!gitRevisionHash.empty()) { sstream << " build from revision " << gitRevisionHash; + } else { + sstream << " built from archive"; } if (dirty) { if (dirty.get()) {