Bash "$#" treated as comment

[GoogleCodeExporter]

Bash's "$#" variable contains the number of arguments.

What steps will reproduce the problem?
1. Try to prettify the included Bash code.

<pre class="lang-bash prettyprint-override"><code># This is a comment
while [[ $# -gt 0 ]]; do
    echo $1
    shift
done
</code></pre>

What is the expected output?  What do you see instead?

The "$#" should be treated as a single token.
Instead, the "#" in "$#" is treated as the start of a comment.

Attached: correct output in vim, incorrect output on StackExchange.

What version are you using?  On what browser?

Unsure; it's whatever Stack Exchange currently uses.
(Sorry!)
Link to JS file: 
https://meta.stackexchange.com/content/Js/prettify-full.en.js?v=37843da05c2b

I'm on Chrome 38.0.2125.111 (Official Build 290379) for Linux Mint (Ubuntu).

Please provide any additional information below.

Keywords: dollar hash, dollar octothorpe, dollar pound, dollar number.

Original issue reported on code.google.com by WChar...@gmail.com on 29 Oct 2014 at 4:36

Attachments:

• stack.png

[GoogleCodeExporter]

Here's the other attachment (sorry).

Original comment by WChar...@gmail.com on 29 Oct 2014 at 4:37

Attachments:

• vim.png