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)
2 # Yes, this intends to be a true POSIX script file.
7 # Parse the tools' paths configuration
8 # It is expected that this script is only to be run from the
9 # source directory of crosstool-NG, so it is trivial to find
10 # paths.mk (we can't use ". paths.mk", as POSIX states that
11 # $PATH should be searched for, and $PATH most probably doe
12 # not include "."), hence the "./".
17 Usage: ${myname} <src_dir> <dst_dir> <base> <inc> [sed_re]
18 Renumbers all patches found in 'src_dir', starting at 'base', with an
19 increment of 'inc', and puts the renumbered patches in 'dst_dir'.
20 Leading digits are replaced with the new indexes, and a subsequent '_'
21 is replaced with a '-'.
22 If 'sed_re' is given, it is interpreted as a valid sed expression, and
23 is be applied to the patch name.
24 If the environment variable FAKE is set to 'y', then nothing gets done,
25 the command to run is only be printed, and not executed (so you can
27 'dst_dir' must not yet exist.
29 patch-renumber.sh patches/gcc/4.2.3 patches/gcc/4.2.4 100 10
30 patch-renumber.sh /some/dir/my-patches patches/gcc/4.3.1 100 10 's/(all[_-])*(gcc[-_])*//;'
34 [ $# -lt 4 -o $# -gt 5 ] && { doUsage; exit 1; }
41 if [ ! -d "${src}" ]; then
42 printf "%s: '%s': not a directory\n" "${myname}" "${src}"
45 if [ -d "${dst}" ]; then
46 printf "%s: '%s': directory already exists\n" "${myname}" "${dst}"
51 if [ -n "${FAKE}" ]; then
52 printf "%s: won't do anything: FAKE='%s'\n" "${myname}" "${FAKE}"
56 ${Q} mkdir -pv "${dst}"
57 for p in "${src}/"*.patch*; do
58 [ -e "${p}" ] || { echo "No such file '${p}'"; exit 1; }
59 newname="$(printf "%03d-%s" \
62 |"${sed}" -r -e 's/^[[:digit:]]+[-_]//' \
66 ${Q} cp -v "${p}" "${dst}/${newname}"