Hacker News Reader

What does "$@@" do? I have used just "$@" for what the script at the end is trying to accomplish, is there some edge case where that fails?

I think that's just the markup for a single @-sign.

Yeah, GNU TeXinfo uses @ as its meta-character, so a source file needs @@ to produce @ in the output.