1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/thesis/scripts/improve-index.sh	Sat Jan 31 20:07:58 2009 +0100
     1.3 @@ -0,0 +1,19 @@
     1.4 +#!/bin/sh
     1.5 +#
     1.6 +# improve index source data and generate the index
     1.7 +
     1.8 +echo "improve-index.sh"
     1.9 +echo "@: $@"
    1.10 +
    1.11 +if [ $# -eq 0 ] ; then
    1.12 +	echo "usage: $0 <idxinput> ..."
    1.13 +	exit 1
    1.14 +fi
    1.15 +
    1.16 +for i in "$@" ; do
    1.17 +	echo "processing $i.idx"
    1.18 +	mv "$i.idx" "$i.unprocessed.idx"
    1.19 +	<"$i.unprocessed.idx" `dirname $0`/improve-index.awk >"$i.idx"
    1.20 +done
    1.21 +
    1.22 +makeindex "$@"