source on github differs from source on torproject

File src/chrome/content/rules/PHP.xml in master branch is different on github and torproject servers. There is bug in this file on second server, while it is not present on github. I thought they should be identical. It confused me for a moment when I was trying to contribute.

$ diff https-everywhere-torproject/src/chrome/content/rules/PHP.xml https-everywhere-github/src/chrome/content/rules/PHP.xml
69a70,73

  <!--    Not secured by server:
                                  -->
  <!--securecookie host="^bugs\.php\.net$" name="^PHPSESSID$" /-->

74c78 < to="https://$1hp.net/" />

          to="https://$1php.net/" />

Trac:
Username: gadelat