add new tools

2022-09-01 09:04:48 +02:00
parent 8358d28942
commit a092056387
5 changed files with 472 additions and 12 deletions
--- a/tools/sync_doc_repo.py
+++ b/tools/sync_doc_repo.py
@ -67,7 +67,7 @@ def process_repositories(args, service):
        elif repo["type"] == 'github':
            repo_url = f"git@github.com:/{repo['repo']}"
        else:
-            logging.error(f"Repository typw {repo['type']} is not supported")
+            logging.error(f"Repository type {repo['type']} is not supported")
            exit(1)
        if not checkout_exists:
            git_repo = Repo.clone_from(