diff options
| -rw-r--r-- | docs/default.do | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/docs/default.do b/docs/default.do index 5f8ee48..a66ed9b 100644 --- a/docs/default.do +++ b/docs/default.do @@ -4,8 +4,9 @@ fn="${1%.*}" case "$1" in - all) redo-ifchange info ;; - info) redo-ifchange cpt.info ;; + all) redo info ;; + allclean) redo ../clean; rm -f cpt.texi ;; + info) redo-ifchange cpt.info cpt.texi cpt.org ;; *.info) redo-ifchange "$fn.texi" $MAKEINFO "$fn.texi" -o "$3" |