complibs/ppl: update GMP location configuration argument for PPL v0.11 and later
'configure' for PPL 0.11 (and later) needs "--with-gmp-prefix" to
provide the location of the GMP toolkit; the previous switches were
"--with-libgmp-prefix" and "--with-libgmpxx-prefix".
The upstream log message is:
commit 08dfb6fea094f8c5a533575a3ea2095edce99a6d
Author: Roberto Bagnara <bagnara@cs.unipr.it>
Date: Sun Jul 12 21:39:46 2009 +0200
New configure option --with-gmp-prefix supersedes the (now removed)
options --with-libgmp-prefix and --with-libgmpxx-prefix.
Link: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=08dfb6fea094f8c5a533575a3ea2095edce99a6d
Since PPL's 'configure' ignores unknown switches, we use all three so we
don't have to conditionalize the ppl.sh build script itself.
Signed-Off-By: Anthony Foiani <anthony.foiani@gmail.com>
(transplanted from 4f0c4fb572e2862c24b28e8d27ce7e9cb9adba65)
1 # Makefile for the scripts/ sub-directory
3 # Here, we can update the config.* scripts.
4 # If we're in CT_LIB_DIR, then CT_LIB_DIR == CT_TOP_DIR, and we can update those
5 # scripts for later inclusion mainline. If CT_LIB_DIR != CT_TOP_DIR, then those
6 # scripts are downloaded only for use in CT_TOP_DIR.
8 # ----------------------------------------------------------
12 @echo ' updatetools - Update the config tools'
14 # ----------------------------------------------------------
15 # Where to get tools from, and where to store them into
16 # The tools are: config.guess and config.sub
18 CONFIG_SUB_SRC="http://git.savannah.gnu.org/gitweb/?p=config.git;a=blob_plain;f=config.sub;hb=HEAD"
19 CONFIG_SUB_DEST=scripts/config.sub
20 CONFIG_GUESS_SRC="http://git.savannah.gnu.org/gitweb/?p=config.git;a=blob_plain;f=config.guess;hb=HEAD"
21 CONFIG_GUESS_DEST=scripts/config.guess
24 updatetools: $(CONFIG_SUB_DEST) $(CONFIG_GUESS_DEST)
26 # ----------------------------------------------------------
27 # How to retrieve the tools
30 ifeq ($(strip $(V)),2)
39 $(CONFIG_SUB_DEST): scripts FORCE
41 $(SILENT)wget $(wget_opt) -O $@ $(CONFIG_SUB_SRC)
42 $(SILENT)chmod u+rwx,go+rx-w $@
44 $(CONFIG_GUESS_DEST): scripts FORCE
46 $(SILENT)wget $(wget_opt) -O $@ $(CONFIG_GUESS_SRC)
47 $(SILENT)chmod u+rwx,go+rx-w $@
49 # ----------------------------------------------------------
53 @$(ECHO) " CLEAN scripts"
54 $(SILENT)[ $(CT_TOP_DIR) = $(CT_LIB_DIR) ] || rm -rf $(CT_TOP_DIR)/scripts