equal
deleted
inserted
replaced
67 FILEBASE=$(basename "$FILE" .tex) |
67 FILEBASE=$(basename "$FILE" .tex) |
68 else |
68 else |
69 FILEBASE=$DIR/$(basename "$FILE" .tex) |
69 FILEBASE=$DIR/$(basename "$FILE" .tex) |
70 fi |
70 fi |
71 |
71 |
72 function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'" } |
72 function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; } |
73 |
73 |
74 |
74 |
75 # operations |
75 # operations |
76 |
76 |
77 function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } |
77 function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } |