That does look to be the problem., thanks. It is a server I want, and the old server (dating back to etch, I have no idea why the successive upgrades all the way to squeeze didn't replace it) was configured at /etc/dhcpd.conf instead of /etc/dhcp/dhcpd.conf. Probably a problem with a long-obsolete upgrade.
I've edited the proper script now, and will try it out as soon as I get the chance to reboot the server to wheezy again. (yes, I dual-boot between squeeze and wheezy; it gives me a useful fallback in case of trouble like this) -- hendrik -- To UNSUBSCRIBE, email to debian-bugs-dist-requ...@lists.debian.org with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org