#!/bin/csh -f
# Make a ``short index'' for file $1
grep "^\\:\{" $1.tex | cat ~ada/tex/indexhead.tex - ~ada/tex/indextail.tex > short$1.tex