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 # Options related to how the build behaves
3 comment "Build behavior"
5 comment "Build options hiden"
10 prompt "Number of parallel jobs" if ! BACKEND
13 Number of jobs make will be allowed to run concurently.
14 Set this higher than the number of processors you have, but not too high.
15 A good rule of thumb is twice the number of processors you have.
17 Enter 1 (or 0) to have only one job at a time.
21 prompt "Maximum allowed load" if ! BACKEND
24 Specifies that no new jobs should be started if there are others jobs
25 running and the load average is at least this value.
27 Makes sense on SMP machines only.
29 Enter 0 to have no limit on the load average.
31 Note: only the integer part of the load is allowed here (you can't enter
36 prompt "Use -pipe" if ! BACKEND
39 Use gcc's option -pipe to use pipes rather than temp files when building
44 prompt "Shell to use as CONFIG_SHELL"
45 default CONFIG_SHELL_BASH
48 config CONFIG_SHELL_SH
50 prompt "sh (the system shell)"
52 Use 'sh' as CONFIG_SHELL.
54 ./configure scripts and Makefiles make intensive use of calling
55 sub-shells. This is usually done by calling /bin/sh. /bin/sh ought
56 to be an at-least-POSIX-conformant shell (that is, able to interpret
59 On many (most?) systems, /bin/sh is a symlink to bash. On some other
60 systems (eg. Ubuntu, latest Debian), /bin/sh points to dash (or ash).
61 bash is a full-featured shell, with many extension to POSIX, but is
62 quite slow (see ection BUGS in the bash man page), while dash is
63 faster, with very few extensions to POSIX. On the other hand, some
64 ./configure scripts, although written to use /bin/sh, may really
65 require to be run by bash.
67 The default is to use bash, as some components (eg. GMP) will fail
68 to build with anything else than bash.
70 config CONFIG_SHELL_ASH
72 prompt "ash (READ HELP!)"
74 Use 'ash' as CONFIG_SHELL.
76 See help for CONFIG_SHELL_SH, above, for more explanations.
78 NOTE: It is advised that you do NOT use ash as CONFIG_SHELL, as some
79 components are broken. If you decide to use ash, and the build breaks,
80 don't come moaning and set the CONFIG_SHELL to bash, below.
82 config CONFIG_SHELL_BASH
86 Use 'bash' as CONFIG_SHELL.
88 See help for CONFIG_SHELL_SH, above, for more explanations.
90 config CONFIG_SHELL_CUSTOM
94 Enter full path to the custom shell below.
96 See help for CONFIG_SHELL_SH, above, for more explanations.
102 default "sh" if CONFIG_SHELL_SH
103 default "ash" if CONFIG_SHELL_ASH
104 default "bash" if CONFIG_SHELL_BASH
105 default "custom" if CONFIG_SHELL_CUSTOM || BACKEND
107 config CONFIG_SHELL_CUSTOM_PATH
109 prompt "Path to custom shell" if ! BACKEND
110 depends on CONFIG_SHELL_CUSTOM || BACKEND