Represent github change ID in status page by PR number

The change.id given to the status.json output for github PRs is a full
"PR#,SHA" combo. This gives it uniqueness when we can have multiple
commits and versions of commits per PR.

When we display this in the status page though i think all we care about
is the PR number, so trim it out and just display that.

Change-Id: I73385a6b0743a6764fdfdd51cd1d8ee02b71c53c
Signed-off-by: Jamie Lennox <jamielennox@gmail.com>

etc/status/public_html/jquery.zuul.js

@@ -279,7 +279,16 @@
 
                 var $change_link = $('<small />');
                 if (change.url !== null) {
-                    if (/^[0-9a-f]{40}$/.test(change.id)) {
+                    var github_id = change.id.match(/^([0-9]+),([0-9a-f]{40})$/);
+                    if (github_id) {
+                        $change_link.append(
+                            $('<a />').attr('href', change.url).append(
+                                $('<abbr />')
+                                    .attr('title', change.id)
+                                    .text('#' + github_id[1])
+                            )
+                        );
+                    } else if (/^[0-9a-f]{40}$/.test(change.id)) {
                         var change_id_short = change.id.slice(0, 7);
                         $change_link.append(
                             $('<a />').attr('href', change.url).append(