diff options
| -rw-r--r-- | rpkid/Makefile.in | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/rpkid/Makefile.in b/rpkid/Makefile.in index 1ec9cc4b..8bf4217b 100644 --- a/rpkid/Makefile.in +++ b/rpkid/Makefile.in @@ -116,7 +116,12 @@ install:: @echo @echo "== Default configuration file location is ${sysconfdir}/rpki.conf ==" @echo - if test -d ${PID_DIR}; then :; else ${INSTALL} -d ${PID_DIR}; fi +# +# We used to do this, but Debian/Ubuntu lintian complained that +# /var/run may be a temporary filesystem, thus directories like this +# should be created at boot. Fair point. +# +# if test -d ${PID_DIR}; then :; else ${INSTALL} -d ${PID_DIR}; fi uninstall deinstall:: xargs rm -fv <installed |