projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 01d8991) | patch
update-copyright: Preserve file permissions. (#5597)
authorMathias Preiner <mathias.preiner@gmail.com>
Fri, 4 Dec 2020 06:32:17 +0000 (22:32 -0800)
committerGitHub <noreply@github.com>
Fri, 4 Dec 2020 06:32:17 +0000 (07:32 +0100)
commit0b7ed19ab13a2bfa6278a0180768a9895aea9aff
tree26817bc9c50ed0f399224961f0a9f0efe7010293tree
parent01d8991ad7059fff4807c2c597c04959d39ab176commit | diff
update-copyright: Preserve file permissions. (#5597)

When updating the copyright headers file permissions were not preserved. In some cases this results in losing the permission to execute scripts. This commit makes sure to preserve the file permissions for updated files.
contrib/update-copyright.pl diff | blob | history