Update from GMP

* admin/update-copyright (updatable_files):
Don’t update copyright year on files copied from GMP, so that
they’re identical to upstream.
* src/mini-gmp.c, src/mini-gmp.h: Copy from GMP development
versions as of 2019-01-01 20:15:39 UTC.

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