aboutsummaryrefslogtreecommitdiff
path: root/docs/default.do
diff options
context:
space:
mode:
Diffstat (limited to 'docs/default.do')
-rw-r--r--docs/default.do2
1 files changed, 1 insertions, 1 deletions
diff --git a/docs/default.do b/docs/default.do
index 1ce12e2..fcf8802 100644
--- a/docs/default.do
+++ b/docs/default.do
@@ -10,7 +10,7 @@ case "$1" in
info) redo-ifchange cpt.info cpt.texi cpt.org ;;
*.info)
# Don't bother if makeinfo doesn't exist on the system, exit with success.
- if ! command -v $MAKEINFO; then
+ if ! command -v $MAKEINFO >/dev/null; then
PHONY
exit 0
fi