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

diff --git a/scripts/retracediff.py b/scripts/retracediff.py
index 413ecac8fffd1ddcf356cfcdaf62907db5d6eac8..171622d03a1ea942b2073e53ee92a2f3feaf264e 100755 (executable)
--- 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__':