4 ms·

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?

• suntuba 4y ago
  I think that's just the markup for a single @-sign.
  • thristian 4y ago
    Yeah, GNU TeXinfo uses @ as its meta-character, so a source file needs @@ to produce @ in the output.