diff options
Diffstat (limited to 'docs')
-rw-r--r-- | docs/default.do | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/docs/default.do b/docs/default.do new file mode 100644 index 0000000..a66ed9b --- /dev/null +++ b/docs/default.do @@ -0,0 +1,27 @@ +. ../config.rc + +# Extensionless name of file +fn="${1%.*}" + +case "$1" in + 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" + ;; + *.texi) + [ -f "$fn.org" ] || exit 0 + redo-ifchange "$fn.org" + cp "$fn.org" "$3.org" + $EMACS "$3.org" --batch -f org-texinfo-export-to-texinfo + rm -f "$3.org" + mv "$3.texi" "$3" + ;; + *) + echo "Unknown target $1" + exit 99 +esac + +PHONY all info html |