is: /usr/lib/php5/man should be: /usr/share/man
No, it shouldn't, it'd cause collisions. *** This bug has been marked as a duplicate of 133007 ***