1#!/bin/sh2# This requires a branch named in $head3# (usually 'man' or 'html', provided by the git.git repository)4set -e5head="$1"6mandir="$2"7SUBDIRECTORY_OK=t8USAGE='<refname> <target directory>'9. git-sh-setup10export GIT_DIR1112test -z "$mandir" && usage13if ! git-rev-parse --verify "$head^0" >/dev/null; then14echo >&2 "head: $head does not exist in the current repository"15usage16fi1718GIT_INDEX_FILE=`pwd`/.quick-doc.index19export GIT_INDEX_FILE20rm -f "$GIT_INDEX_FILE"21git-read-tree $head22git-checkout-index -a -f --prefix="$mandir"/2324if test -n "$GZ"; then25cd "$mandir"26for i in `git-ls-tree -r --name-only $head`27do28gzip < $i > $i.gz && rm $i29done30fi31rm -f "$GIT_INDEX_FILE"