make the name of the library directory a config option

diff --git a/Documentation/install-doc-quick.sh b/Documentation/install-doc-quick.sh
index a64054948aec41e820b8864a71229bbd568aa99a..e6601bdd8237bbda80727780434d5b9d337e8bf4 100755 (executable)
--- a/Documentation/install-doc-quick.sh
+++ b/Documentation/install-doc-quick.sh
@@ -10,7 +10,7 @@ USAGE='<refname> <target directory>'
 export GIT_DIR
 
 test -z "$mandir" && usage
-if ! git-rev-parse --verify "$head^0" >/dev/null; then
+if ! git rev-parse --verify "$head^0" >/dev/null; then
        echo >&2 "head: $head does not exist in the current repository"
        usage
 fi
@@ -18,12 +18,12 @@ fi
 GIT_INDEX_FILE=`pwd`/.quick-doc.index
 export GIT_INDEX_FILE
 rm -f "$GIT_INDEX_FILE"
-git-read-tree $head
-git-checkout-index -a -f --prefix="$mandir"/
+git read-tree $head
+git checkout-index -a -f --prefix="$mandir"/
 
 if test -n "$GZ"; then
        cd "$mandir"
-       for i in `git-ls-tree -r --name-only $head`
+       for i in `git ls-tree -r --name-only $head`
        do
                gzip < $i > $i.gz && rm $i
        done