-# update the local 'man' and 'html' branches with pregenerated output files, for
-# people who don't have pandoc (and maybe to aid in google searches or something)
-export-docs: Documentation/all
- git update-ref refs/heads/man origin/man '' 2>/dev/null || true
- git update-ref refs/heads/html origin/html '' 2>/dev/null || true
- set -eo pipefail; \
- GIT_INDEX_FILE=gitindex.tmp; export GIT_INDEX_FILE; \
- rm -f $${GIT_INDEX_FILE} && \
- git add -f Documentation/*.1 && \
- git update-ref refs/heads/man \
- $$(echo "Autogenerated man pages for $$(git describe --always)" \
- | git commit-tree $$(git write-tree --prefix=Documentation) \
- -p refs/heads/man) && \
- rm -f $${GIT_INDEX_FILE} && \
- git add -f Documentation/*.html && \
- git update-ref refs/heads/html \
- $$(echo "Autogenerated html pages for $$(git describe --always)" \
- | git commit-tree $$(git write-tree --prefix=Documentation) \
- -p refs/heads/html)
+# Note: this adds commits containing the current manpages in roff and
+# html format to the man and html branches respectively. The version
+# is determined by "git describe --always".
+.PHONY: update-doc-branches
+update-doc-branches: Documentation/all
+ dev/update-doc-branches refs/heads/man refs/heads/html