diff options
author | Jan Holthuis <jan.holthuis@ruhr-uni-bochum.de> | 2021-04-15 18:11:51 +0200 |
---|---|---|
committer | Jan Holthuis <jan.holthuis@ruhr-uni-bochum.de> | 2021-04-16 00:44:28 +0200 |
commit | d7ab3f3dc32eb6fa86da2ddc147eedcc2b82399d (patch) | |
tree | 7b862ea1630e0bc062d1c24ab4b06546b1ed7b05 | |
parent | eeeda76092ed2b73738081170fdaa0a9b7265b41 (diff) |
tools/deploy.py: Add `--dirty` flag to git describe for local usage
-rw-r--r-- | tools/deploy.py | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tools/deploy.py b/tools/deploy.py index 372968027e..774ad3ce31 100644 --- a/tools/deploy.py +++ b/tools/deploy.py @@ -66,7 +66,9 @@ def git_info(info, path="."): elif info == "commit": cmd = ("git", "rev-parse", "HEAD") elif info == "describe": - cmd = ("git", "describe") + # A dirty git state should only be possible on local builds, but since + # this script may be used locally we'll add it here. + cmd = ("git", "describe", "--dirty") else: raise ValueError("Invalid git info type!") |