Version info includes whether the git repo is dirty

Author: mernst

framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java

@@ -2713,13 +2713,19 @@ private String getCheckerVersion() {
  throw new BugInCF("Could not find the version in git.properties");
  }
  String branch = gitProperties.getProperty("git.branch");
- if (version.endsWith("-SNAPSHOT") || !branch.equals("master")) {
+ // git.dirty indicates modified tracked files and staged changes. Untracked content doesn't
+ // count, so not being dirty doesn't mean that exactly the printed commit is being run.
+ String dirty = gitProperties.getProperty("git.dirty");
+ if (version.endsWith("-SNAPSHOT") || !branch.equals("master") || dirty.equals("true")) {
  // Sometimes the branch is HEAD, which is not informative.
  // How does that happen, and how can I fix it?
  version += ", branch " + branch;
  // For brevity, only date but not time of day.
  version += ", " + gitProperties.getProperty("git.commit.time").substring(0, 10);
  version += ", commit " + gitProperties.getProperty("git.commit.id.abbrev");
+ if (dirty.equals("true")) {
+ version += ", dirty=true";
+ }
  }
  return version;
  }