From 5531b128001ec6cc71164cdf2a5f94d3eb733812 Mon Sep 17 00:00:00 2001
From: Artem Goncharov <artem.goncharov@gmail.com>
Date: Wed, 23 Nov 2022 13:49:51 +0100
Subject: [PATCH] do not create PR when no changes required

---
 tools/sync_doc_repo.py | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/tools/sync_doc_repo.py b/tools/sync_doc_repo.py
index 05e6124b..cc1e5d4c 100644
--- a/tools/sync_doc_repo.py
+++ b/tools/sync_doc_repo.py
@@ -120,6 +120,10 @@ def process_repositories(args, service):
             dirs_exist_ok=True
         )
         repo_to.index.add([doc["rst_location"]])
+        if len(repo_to.index.diff("HEAD")) == 0:
+            # Nothing to commit
+            logging.debug("No changes.")
+            continue
         repo_to.index.commit(
             (
                 f"Synchronize {doc['title']}\n\n"