doc-sync: add man/ to the passed directory

This mirrors the behaviour before multiple version support

diff --git a/tools/sync-docs.py b/tools/sync-docs.py
index bab99f8cb344348029330bfec2000ff439e112f4..eab425e718bc86a355c5bb81a6086f3688b5b89e 100755 (executable)
--- a/tools/sync-docs.py
+++ b/tools/sync-docs.py
@@ -108,7 +108,7 @@ def main(version, directory, www_target, latest):
                 "--exclude=*",
                 "--omit-dir-times",
                 directory + "/",  # copy contents of directory
-                os.path.join(www_target, d),
+                os.path.join(www_target, "man", d),
             ]
         )
 
@@ -118,7 +118,7 @@ def main(version, directory, www_target, latest):
             "-v",
             os.path.join(directory, "index.json"),
             os.path.join(directory, "nav.js"),
-            www_target,
+            os.path.join(www_target, "man"),
         ]
     )