diff options
Diffstat (limited to 'manual/appnotes.sh')
| -rwxr-xr-x | manual/appnotes.sh | 22 |
1 files changed, 0 insertions, 22 deletions
diff --git a/manual/appnotes.sh b/manual/appnotes.sh deleted file mode 100755 index 0ae52862e..000000000 --- a/manual/appnotes.sh +++ /dev/null @@ -1,22 +0,0 @@ -#!/bin/bash - -set -ex -for job in APPNOTE_010_Verilog_to_BLIF APPNOTE_011_Design_Investigation APPNOTE_012_Verilog_to_BTOR -do - [ -f $job.ok -a $job.ok -nt $job.tex ] && continue - if [ -f $job/make.sh ]; then - cd $job - bash make.sh - cd .. - fi - old_md5=$([ -f $job.aux ] && md5sum < $job.aux || true) - while - pdflatex -shell-escape -halt-on-error $job.tex || exit - new_md5=$(md5sum < $job.aux) - [ "$old_md5" != "$new_md5" ] - do - old_md5="$new_md5" - done - touch $job.ok -done - |