diff options
Diffstat (limited to 'stdlib')
| -rw-r--r-- | stdlib/Makefile | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/stdlib/Makefile b/stdlib/Makefile index 6db064d543..85a5347d32 100644 --- a/stdlib/Makefile +++ b/stdlib/Makefile @@ -113,7 +113,9 @@ $(mpn-copy): %: $(ignore gmp2glibc.sed) $(gmp-srcdir)/%; $(gmp2glibc) .PHONY: copy-mpn clean-mpn mpn-stuff mpn-stuff: $(mpn-stuff) copy-mpn: $(mpn-stuff) +ifeq ($(with-cvs),yes) test ! -d CVS || cvs $(CVSOPTS) commit -m'Updated from $(gmp-srcdir)' $+ +endif clean-mpn: rm -f $(mpn-stuff) |