diff options
-rw-r--r-- | src/Makefile.am | 6 | ||||
-rwxr-xr-x | tools/get_patches.sh | 11 |
2 files changed, 14 insertions, 3 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 345743a5f..8bb4d731c 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -90,8 +90,10 @@ libmpfr_la_LIBADD = @LIBOBJS@ # 4.0.x 6:x:0 libmpfr_la_LDFLAGS = $(MPFR_LDFLAGS) $(LIBMPFR_LDFLAGS) -version-info 6:0:0 -get_patches.c: $(top_srcdir)/tools/get_patches.sh $(top_srcdir)/PATCHES - $< > $@ || rm -f $@ +GET_PATCHES_SH = $(top_srcdir)/tools/get_patches.sh +PATCHES = $(top_srcdir)/PATCHES +get_patches.c: $(GET_PATCHES_SH) $(PATCHES) + $(GET_PATCHES_SH) $(PATCHES) > $@ || { rm -f $@; exit 1; } if MINI_GMP diff --git a/tools/get_patches.sh b/tools/get_patches.sh index cf3912ee7..5d93c3926 100755 --- a/tools/get_patches.sh +++ b/tools/get_patches.sh @@ -1,5 +1,14 @@ #!/bin/sh +set -e + +if [ $# -ne 1 ]; then + echo "Usage: $0 <PATCHES_file>" >&2 + exit 1 +fi + +patches=`cat "$1"` + cat <<EOF /* mpfr_get_patches -- Patches that have been applied @@ -30,5 +39,5 @@ mpfr_get_patches (void) { EOF -echo ' return "'`cat PATCHES`'";' +echo " return \"$patches\";" echo '}' |