Fix making dev version for release tags

glue/python/overwrite_dev_version_with_date.py

@@ -1,5 +1,7 @@
 #########################################################
 # Sets version numbers to a date-based dev version.
+#
+# Does nothing if not on a dev version.
 #########################################################
 # Example usage (from repo root):
 #
@@ -22,6 +24,8 @@ def main():
  with open('setup.py') as f:
  maj_min_version_line, = [line for line in f.read().splitlines() if re.match("^version = '[^']+'", line)]
  maj_version, min_version, patch = maj_min_version_line.split()[-1].strip("'").split('.')
+ if 'dev' not in patch:
+ return # Do nothing for non-dev versions.
  timestamp = subprocess.check_output(['git', 'show', '-s', '--format=%ct', 'HEAD']).decode().strip()
  new_version = f"{maj_version}.{min_version}.dev{timestamp}"