lib/Tools/latex
changeset 8568 b18540435f26
parent 8565 3c3895e37761
child 9788 df671fa2562a
     1.1 --- a/lib/Tools/latex	Fri Mar 24 13:48:31 2000 +0100
     1.2 +++ b/lib/Tools/latex	Fri Mar 24 14:40:51 2000 +0100
     1.3 @@ -69,7 +69,7 @@
     1.4    FILEBASE=$DIR/$(basename "$FILE" .tex)
     1.5  fi
     1.6  
     1.7 -function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'" }
     1.8 +function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; }
     1.9  
    1.10  
    1.11  # operations