From da71c8b722ef2a28c6c3ba874bf45dfb00eaf9a9 Mon Sep 17 00:00:00 2001
From: Tom Poole <thomas.poole@roli.com>
Date: Wed, 25 Sep 2019 12:40:16 +0100
Subject: [PATCH] Documentation:  Fixed a Doxygen generation issue

---
 doxygen/process_source_files.py | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/doxygen/process_source_files.py b/doxygen/process_source_files.py
index 376c97db2b..d9862ff708 100644
--- a/doxygen/process_source_files.py
+++ b/doxygen/process_source_files.py
@@ -75,8 +75,10 @@ if __name__ == "__main__":
                              "subdirectories")
     args = parser.parse_args()
 
-    try: 
+    try:
         shutil.rmtree(args.dest_dir)
+    except OSError:
+        pass
     except FileNotFoundError:
         pass