diff options
-rwxr-xr-x | tools/sync-docs.py | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tools/sync-docs.py b/tools/sync-docs.py index 95436e2710..86fe1a8ed7 100755 --- 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() |