Re-try the file copy once if it fails. This works around an obscure and non-reproduci...

diff --git a/Mac/scripts/MkDistr.py b/Mac/scripts/MkDistr.py
index f446b343c51147ef35a77cc1610cc1efe7fd63e6..3e2ee27f0e02f1187573bd203b947885740925de 100644 (file)
--- a/Mac/scripts/MkDistr.py
+++ b/Mac/scripts/MkDistr.py
@@ -292,9 +292,15 @@ class Main:
                                                try:
                                                        macostools.copy(fullname, os.path.join(destprefix, dest), 1)
                                                except: #DBG
-                                                       print 'cwd', os.getcwd() #DBG
-                                                       print 'fsspec', macfs.FSSpec(fullname) #DBG
-                                                       raise
+                                                       print '*** Copy failed mysteriously, try again'
+                                                       print '*** cwd', os.getcwd() #DBG
+                                                       print '*** fsspec', macfs.FSSpec(fullname) #DBG
+                                                       # Get rid of open files
+                                                       try:
+                                                               i = 1 / 0
+                                                       except:
+                                                               pass
+                                                       macostools.copy(fullname, os.path.join(destprefix, dest), 1)
                for d in todo:
                        if not self.rundir(d, destprefix, doit):
                                rv = 0