diff options
Diffstat (limited to 'admin/update-copyright')
| -rwxr-xr-x | admin/update-copyright | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/admin/update-copyright b/admin/update-copyright index 44cb84d8cc9..9f360904ce6 100755 --- a/admin/update-copyright +++ b/admin/update-copyright @@ -50,6 +50,7 @@ repo_files=$(git ls-files) && # Do not update the copyright of files that have one or more of the # following problems: # . They are license files, maintained by the FSF, with their own dates. +# . They are GMP files, maintained by the GMP project, with their own dates. # . Their format cannot withstand changing the contents of copyright strings. updatable_files=$(find $repo_files \ @@ -70,6 +71,7 @@ updatable_files=$(find $repo_files \ ! -name hand.cur \ ! -name key.pub \ ! -name key.sec \ + ! -name 'mini-gmp.[ch]' \ -print) && build-aux/update-copyright $updatable_files |