meillo@372: #!/bin/sh
meillo@372: #
meillo@372: # improve index source data and generate the index
meillo@372: 
meillo@372: echo "improve-index.sh"
meillo@372: echo "@: $@"
meillo@372: 
meillo@372: if [ $# -eq 0 ] ; then
meillo@372: 	echo "usage: $0 <idxinput> ..."
meillo@372: 	exit 1
meillo@372: fi
meillo@372: 
meillo@372: for i in "$@" ; do
meillo@372: 	echo "processing $i.idx"
meillo@372: 	mv "$i.idx" "$i.unprocessed.idx"
meillo@372: 	<"$i.unprocessed.idx" `dirname $0`/improve-index.awk >"$i.idx"
meillo@372: done
meillo@372: 
meillo@372: makeindex "$@"