Handle filenames containing $ characters

Like double quotes, $ signs are also problematic when used inside the
name of tex files. We now show an error message if a filename contains
such a character.