equal
deleted
inserted
replaced
68 function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; } |
68 function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; } |
69 |
69 |
70 |
70 |
71 # operations |
71 # operations |
72 |
72 |
73 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } |
73 function run_pdflatex () { $ISABELLE_PDFLATEX "$FILEBASE.tex"; } |
74 function run_bibtex () { |
74 function run_bibtex () { |
75 $ISABELLE_BIBTEX </dev/null "$FILEBASE" |
75 $ISABELLE_BIBTEX </dev/null "$FILEBASE" |
76 RC="$?" |
76 RC="$?" |
77 if [ "$RC" -gt 0 -a -f "${FILEBASE}.blg" ]; then |
77 if [ "$RC" -gt 0 -a -f "${FILEBASE}.blg" ]; then |
78 perl -n -e 'if (m/^I (found no.*$)/) { print "bibtex $1\n"; }' "${FILEBASE}.blg" >&2 |
78 perl -n -e 'if (m/^I (found no.*$)/) { print "bibtex $1\n"; }' "${FILEBASE}.blg" >&2 |