diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2020-12-07 08:57:17 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2020-12-07 08:57:17 -0600 |
| commit | 1d21e11dc18e8c290ed0b085ca51844cc6d70019 (patch) | |
| tree | 2291cd30fb5f6651fa10307ba54598fab4691739 /contrib | |
| parent | 9a69af74e2935a6ecf8d867b1394a4fcfbbd38b7 (diff) | |
| parent | 85f14a1ba37949afbd33f38c8565dc5d45a300fe (diff) | |
Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-new
Diffstat (limited to 'contrib')
| -rwxr-xr-x | contrib/update-copyright.pl | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl index 1f119d8e9..6a8482e76 100755 --- a/contrib/update-copyright.pl +++ b/contrib/update-copyright.pl @@ -257,6 +257,11 @@ sub handleFile { print $OUT $_; } close $OUT; + + # Preserve file permissions of $infile + my $perm = (stat($infile))[2] & 0777; + chmod $perm, $outfile; + rename($outfile, $infile) || die "can't rename working file \`$outfile' to \`$infile'"; } |