# HG changeset patch # User wenzelm # Date 1343305467 -7200 # Node ID 3e17f343deb580d596e152b01f050be59a195d9b # Parent 84df8858c8acc0edd5668355103f28b438b3a500 allow spaces in file names; diff -r 84df8858c8ac -r 3e17f343deb5 lib/Tools/latex --- a/lib/Tools/latex Thu Jul 26 14:22:37 2012 +0200 +++ b/lib/Tools/latex Thu Jul 26 14:24:27 2012 +0200 @@ -62,8 +62,8 @@ # root file -DIR=$(dirname "$FILE") -FILEBASE=$(basename "$FILE" .tex) +DIR="$(dirname "$FILE")" +FILEBASE="$(basename "$FILE" .tex)" [ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE" function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; }