retracediff: Avoid WindowsError 5 Access is denied, when exiting.

1 files changed, 10 insertions, 2 deletions

diff --git a/scripts/retracediff.py b/scripts/retracediff.py
index 413ecac8..171622d0 100755
--- a/scripts/retracediff.py
+++ b/scripts/retracediff.py
@@ -269,9 +269,17 @@ def main():
 
                 highligher.flush()
         finally:
-            src_proc.terminate()
+            try:
+                src_proc.terminate()
+            except OSError:
+                # Avoid http://bugs.python.org/issue14252
+                pass
     finally:
-        ref_proc.terminate()
+        try:
+            ref_proc.terminate()
+        except OSError:
+            # Avoid http://bugs.python.org/issue14252
+            pass
 
 
 if __name__ == '__main__':