Fix making dev version for release tags

Author: Strilanc

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}"