fix: close patch_file before deleting it (#15055)

This commit is contained in:
Heilig Benedek 2018-10-10 15:55:25 +02:00 committed by Charles Kerr
parent 539d6d20b7
commit 2d186cb31a

View file

@ -325,6 +325,7 @@ def main():
retcode = ExitStatus.DIFF retcode = ExitStatus.DIFF
if patch_file.tell() == 0: if patch_file.tell() == 0:
patch_file.close()
os.unlink(patch_file.name) os.unlink(patch_file.name)
else: else:
print("\nTo patch these files, run:\n$ git apply {}\n" print("\nTo patch these files, run:\n$ git apply {}\n"