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