30 Jul
2010
30 Jul
'10
10:15 a.m.
Three options then:
1. Install header files (etc.) in /usr/include/pike7.8/pike instead of /usr/include/pike7.8. The department of redundancy department may complain.
2. Install header files (etc.) in /usr/include/pike. This means that only one pike*-dev can be installed at any time, which makes it impossible to build module packages supporting multiple Pike versions.
3. Force Debian users to use #include <pike7.8/stuff.h>. Not good.