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

[Bill Allombert]

On Sun, Jul 07, 2013 at 01:35:58PM -0500, Steve M. Robbins wrote:
> 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/

I has reported the problem and Simon Paillard has fixed packages.debian.org to
display ppc64 packages too. Sorry for the confusion.

Cheers,
-- 
Bill. <ballombe at debian.org>

Imagine a large red swirl here.