Bug#784096: pps-tools: Please provide a -dev package

2015-05-03 Thread Vincent Blut
Le dim. 3 mai 2015 à 16:40, Bernd Zeimetz a écrit : severity 784096 wishlist tags 784096 wontfix thanks hi, Hi, with my pps-tools and gpsd maintainer hat on I say: Installed-Size: 76 is so tiny that I can't see a reason to create a single package for a single 5k header file. Well, ma

Bug#784096: pps-tools: Please provide a -dev package

2015-05-03 Thread Bernd Zeimetz
severity 784096 wishlist tags 784096 wontfix thanks hi, with my pps-tools and gpsd maintainer hat on I say: Installed-Size: 76 is so tiny that I can't see a reason to create a single package for a single 5k header file. cheers, bernd On 05/03/2015 02:55 AM, Vincent Blut wrote: > Package: pp

Bug#784096: pps-tools: Please provide a -dev package

2015-05-02 Thread Vincent Blut
Package: pps-tools Severity: normal Hi, It would be great to split the header file from the 'pps-tools' package. I maintain a package (chrony) which can be enhanced by providing PPSAPI support (RFC 2783), but currently I have no choice but to build-depend on the whole thing which is cumbersome. A