Bug#714998: lib32gmp-dev: non standard header file path

[Steve M. Robbins]

On July 7, 2013 06:58:12 AM Bill Allombert wrote:

> > I don't really track the various ports, so I'm not sure what you mean by
> > "proper".  Does http://wiki.debian.org/PPC64 not work for you?
> 
> You can easily check on <http://packages.debian.org/sid/libgmp-dev> that
> there is no libgmp-dev packages for ppc64.

But, per the wiki instructions, you can find it here:  
http://ftp.de.debian.org/debian-ports/pool-ppc64/main/g/gmp/

Do you have a PPC64?  Can you test that these indeed work?  I presume they do, 
since the build ran unit tests (http://buildd.debian-
ports.org/status/fetch.php?pkg=gmp&arch=ppc64&ver=2%3A5.1.2%2Bdfsg-2&stamp=1372684640).

-Steve