7 if awk -f extract.awk -vexname=$fig $input > /dev/null; then
8 echo generating ${fig}.dot
9 opt=`awk -f extract.awk -vexname=$fig $input |
10 sed '/^ *OPT:/s/^.*: *//p;d'`
11 awk -f extract.awk -vexname=$fig $input > ${fig}.rl
12 ../ragel/ragel -V -p ${fig}.rl > ${fig}.dot
14 echo "$0: internal error: figure $fig not found in $input" >&2