hcoop-krb5-config for Debian ----------------------------