diff options
| -rw-r--r-- | gmp/Makefile | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/gmp/Makefile b/gmp/Makefile index 750dfb6c6c..13faf9f170 100644 --- a/gmp/Makefile +++ b/gmp/Makefile @@ -99,10 +99,15 @@ libgmp.dll.a: libgmp-3.dll endif endif +# GMP takes a long time to build, but changes rarely. Hence we don't +# bother cleaning it before validating, because that adds a +# significant overhead to validation. +ifeq "$(Validating)" "NO" clean distclean maintainer-clean :: $(RM) -f stamp.gmp.static stamp.gmp.shared $(RM) -rf gmpbuild $(RM) -rf gmpbuild-shared +endif #----------------------------------------------------------------------------- # |