ef9e57843d
make an entire system work nicely with DESTDIR (to say nothing of being able to move from /usr/local to somewhere else).