Merge branch 'pb/remote-mirror-config'
commitdc484f2213a34ced5abe5eb968650035204b6035
authorJunio C Hamano <gitster@pobox.com>
Tue, 6 May 2008 02:15:39 +0000 (5 19:15 -0700)
committerJunio C Hamano <gitster@pobox.com>
Tue, 6 May 2008 02:15:39 +0000 (5 19:15 -0700)
tree1e1d0d7563cc91bd52ffcb895b9f21a0ed2607c8
parent2b3e60c245684fd68bab36c07fee9888ff24f4b4
parent84bb2dfd9f4873c9ca19537efe62219b09ec03bf
Merge branch 'pb/remote-mirror-config'

* pb/remote-mirror-config:
  Add a remote.*.mirror configuration option
Documentation/config.txt
Documentation/git-push.txt
builtin-remote.c
remote.c