aboutsummaryrefslogtreecommitdiff
path: root/docs/default.do
diff options
context:
space:
mode:
Diffstat (limited to 'docs/default.do')
-rw-r--r--docs/default.do5
1 files changed, 5 insertions, 0 deletions
diff --git a/docs/default.do b/docs/default.do
index a66ed9b..3519aec 100644
--- a/docs/default.do
+++ b/docs/default.do
@@ -8,6 +8,11 @@ case "$1" in
allclean) redo ../clean; rm -f cpt.texi ;;
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
+ PHONY
+ exit 0
+ fi
redo-ifchange "$fn.texi"
$MAKEINFO "$fn.texi" -o "$3"
;;