[PPL-devel] [GIT] ppl/ppl(master): New configure options `--with-gmp=DIR', `--with-gmp-include=DIR' and

[Roberto Bagnara]

Module: ppl/ppl
Branch: master
Commit: 1f0282c0cb86a7a9d86fb21721b985bab2b60bd5
URL:    http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1f0282c0cb86a7a9d86fb21721b985bab2b60bd5

Author: Roberto Bagnara <bagnara at cs.unipr.it>
Date:   Sat Jul 23 12:36:26 2011 +0200

New configure options `--with-gmp=DIR', `--with-gmp-include=DIR' and
`--with-gmp-lib=DIR'.
These supersede the (now removed) option `--with-gmp-prefix'.
(The old option never really worked; hopefully this is the last change
in this area.)

---

 NEWS               |   15 +-
 configure.ac       |    4 +-
 m4/Makefile.am     |    3 -
 m4/ac_check_gmp.m4 |   67 +++--
 m4/lib-ld.m4       |  109 --------
 m4/lib-link.m4     |  777 ----------------------------------------------------
 m4/lib-prefix.m4   |  224 ---------------
 7 files changed, 51 insertions(+), 1148 deletions(-)

Diff:   http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=1f0282c0cb86a7a9d86fb21721b985bab2b60bd5