projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
54d24c7
)
Remove trailing slashes from directories if specified via command line.
author
Mathias Preiner
<mathias.preiner@gmail.com>
Tue, 11 Jul 2017 18:55:54 +0000
(11:55 -0700)
committer
Mathias Preiner
<mathias.preiner@gmail.com>
Tue, 11 Jul 2017 18:55:54 +0000
(11:55 -0700)
contrib/update-copyright.pl
patch
|
blob
|
history
diff --git
a/contrib/update-copyright.pl
b/contrib/update-copyright.pl
index 9458bb14defedb60bb7ededbbb424339e6dbda56..5f31f48c911e09bcc66d88c09643c0ba494f02f6 100755
(executable)
--- a/
contrib/update-copyright.pl
+++ b/
contrib/update-copyright.pl
@@
-117,6
+117,7
@@
print "Updating sources...\n";
while($#searchdirs >= 0) {
my $dir = shift @searchdirs;
+ $dir =~ s,\/$,,; # remove trailing slash from directory
my $mode = (stat($dir))[2] || warn "file or directory \`$dir' does not exist!";
my $is_directory = S_ISDIR($mode);
if($is_directory) {