configure: rename --with-gmp_include and --with-gmp_library to --with-gmp-include...
commitb8622a7e850a9eb10b19b4f5d2f4e8a1a22fa5aa
authorSebastian Pop <sebastian.pop@inria.fr>
Wed, 21 Feb 2007 10:10:40 +0000 (21 11:10 +0100)
committerSven Verdoolaege <skimo@kotnet.org>
Wed, 21 Feb 2007 12:23:58 +0000 (21 13:23 +0100)
tree6cd42f24bbd277e0485d13b46111f0e44fb8c2a9
parent1ed1689906e6bd6cbcecc2419044aac952051639
configure: rename --with-gmp_include and --with-gmp_library to --with-gmp-include and --with-gmp-library
configure.in