# 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'"; }