| Index: Source/bindings/scripts/utilities.py
|
| diff --git a/Source/bindings/scripts/utilities.py b/Source/bindings/scripts/utilities.py
|
| index 2a1ec0ab807f6d0a562fef5918cbad7027f0de54..7a7a3e69f874fd98a634b871080dc63a363aad05 100644
|
| --- a/Source/bindings/scripts/utilities.py
|
| +++ b/Source/bindings/scripts/utilities.py
|
| @@ -39,8 +39,12 @@ def write_file(new_text, destination_filename, only_if_changed):
|
| def write_pickle_file(pickle_filename, data, only_if_changed):
|
| if only_if_changed and os.path.isfile(pickle_filename):
|
| with open(pickle_filename) as pickle_file:
|
| - if pickle.load(pickle_file) == data:
|
| - return
|
| + try:
|
| + if pickle.load(pickle_file) == data:
|
| + return
|
| + except (EOFError, pickle.UnpicklingError):
|
| + # If trouble unpickling, overwrite
|
| + pass
|
| with open(pickle_filename, 'w') as pickle_file:
|
| pickle.dump(data, pickle_file)
|
|
|
|
|