doc-sync: strip point release from version before uploading

We create subdirectories for each major release, but not for point releases
so strip the suffix if it is present

diff --git a/tools/sync-docs.py b/tools/sync-docs.py
index 95436e2710a09928b371971ad33979129187e213..86fe1a8ed7eac8d745b05d3c3a646e0b6effc747 100755 (executable)
--- a/tools/sync-docs.py
+++ b/tools/sync-docs.py
@@ -94,6 +94,8 @@ def get_latest_version():
 def main(version, directory, www_target):
     index_filename = os.path.join(directory, "index.json")
     nav_filename = os.path.join(directory, "nav.js")
+    # The upload directory does not contain point release suffixes
+    version = re.sub(r"\..+$", "", version)
 
     current_branch = subprocess.check_output(["git", "branch", "--show-current"], text=True).strip()