The pages under are built from Documentation/ directory of the git.git project and needed to be kept up-to-date. The servers are mirrored and I was told that the origin of the mirror is on the machine $, on which I was given an account when I took over Git maintainership from Linus.

The directories relevant to this how-to are these two:

/pub/scm/git/git.git/	The public Git repository.
/pub/software/scm/git/docs/	The HTML documentation page.

So I made a repository to generate the documentation under my home directory over there.

$ cd
$ mkdir doc-git && cd doc-git
$ git clone /pub/scm/git/git.git/ docgen

What needs to happen is to update the $HOME/doc-git/docgen/ working tree, build HTML docs there and install the result in /pub/software/scm/git/docs/ directory. So I wrote a little script:

$ cat > <<\EOF
cd $HOME/doc-git/docgen || exit
unset GIT_DIR
git pull /pub/scm/git/git.git/ master &&
cd Documentation &&
make install-webdoc

Initially I used to run this by hand whenever I push into the public Git repository. Then I did a cron job that ran twice a day. The current round uses the post-update hook mechanism, like this:

$ cat >/pub/scm/git/git.git/hooks/post-update <<\EOF
# An example hook script to prepare a packed repository for use over
# dumb transports.
# To enable this hook, make this file executable by "chmod +x post-update".
case " $* " in
*' refs/heads/master '*)
        echo $HOME/doc-git/ | at now
exec git-update-server-info
$ chmod +x /pub/scm/git/git.git/hooks/post-update

There are four things worth mentioning: