Documentation: explain push.default option a bit more

diff --git a/Documentation/howto-index.sh b/Documentation/howto-index.sh
index f9d3e57a9179d86389ce4b3f56e34431f1e9a4a7..34aa30c5b9ffc617e1519878317c2ae83bed6a6a 100755 (executable)
--- a/Documentation/howto-index.sh
+++ b/Documentation/howto-index.sh
@@ -41,7 +41,14 @@ do
                q
        }' "$txt"`
 
-       echo "* link:$txt[$title] $from
+       if grep 'Content-type: text/asciidoc' >/dev/null $txt
+       then
+               file=`expr "$txt" : '\(.*\)\.txt$'`.html
+       else
+               file="$txt"
+       fi
+
+       echo "* link:$file[$title] $from
 $abstract
 
 "