lib/Tools/latex

   FILEBASE=$(basename "$FILE" .tex)
 else
   FILEBASE=$DIR/$(basename "$FILE" .tex)
 fi
 
-function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'" }
+function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; }
 
 
 # operations
 
 function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }