diff options
| -rwxr-xr-x | scripts/verify-bashisms | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/scripts/verify-bashisms b/scripts/verify-bashisms index 28795f4cc7..ed0a5631d0 100755 --- a/scripts/verify-bashisms +++ b/scripts/verify-bashisms @@ -114,3 +114,4 @@ if __name__=='__main__': for message,source in results: print(" %s\n %s" % (message, source)) print() + tinfoil.shutdown() |