equal
deleted
inserted
replaced
60 |
60 |
61 ## main |
61 ## main |
62 |
62 |
63 # root file |
63 # root file |
64 |
64 |
65 DIR=$(dirname "$FILE") |
65 DIR="$(dirname "$FILE")" |
66 FILEBASE=$(basename "$FILE" .tex) |
66 FILEBASE="$(basename "$FILE" .tex)" |
67 [ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE" |
67 [ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE" |
68 |
68 |
69 function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; } |
69 function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; } |
70 |
70 |
71 |
71 |