git-remote-mediawiki: more efficient 'pull' in the best case
[git/raj.git] / Documentation / technical / api-index.sh
blob9c3f4131b8586408acd81d1e60912b51688575ed
1 #!/bin/sh
4 c=////////////////////////////////////////////////////////////////
5 skel=api-index-skel.txt
6 sed -e '/^\/\/ table of contents begin/q' "$skel"
7 echo "$c"
9 ls api-*.txt |
10 while read filename
12 case "$filename" in
13 api-index-skel.txt | api-index.txt) continue ;;
14 esac
15 title=$(sed -e 1q "$filename")
16 html=${filename%.txt}.html
17 echo "* link:$html[$title]"
18 done
19 echo "$c"
20 sed -n -e '/^\/\/ table of contents end/,$p' "$skel"
21 ) >api-index.txt+
23 if test -f api-index.txt && cmp api-index.txt api-index.txt+ >/dev/null
24 then
25 rm -f api-index.txt+
26 else
27 mv api-index.txt+ api-index.txt