diff options
Diffstat (limited to 'doc/ragel/genfigs.sh')
-rwxr-xr-x | doc/ragel/genfigs.sh | 18 |
1 files changed, 0 insertions, 18 deletions
diff --git a/doc/ragel/genfigs.sh b/doc/ragel/genfigs.sh deleted file mode 100755 index 8d521075..00000000 --- a/doc/ragel/genfigs.sh +++ /dev/null @@ -1,18 +0,0 @@ -#!/bin/bash -# - -input=ragel-guide.tex - -for fig; do - if awk -f extract.awk -vexname=$fig $input > /dev/null; then - echo generating ${fig}.dot - opt=`awk -f extract.awk -vexname=$fig $input | - sed '/^ *OPT:/s/^.*: *//p;d'` - awk -f extract.awk -vexname=$fig $input > ${fig}.rl - ../ragel/ragel -V -p ${fig}.rl > ${fig}.dot - else - echo "$0: internal error: figure $fig not found in $input" >&2 - exit 1 - fi -done - |