Convert <!-- timing data --> to a <script></script> block

Convert <!-- timing data --> to a <script></script> block

This patch replaces:

  <!-- Served by mw1069 in 0.976 secs. -->

With:

  <script>mw.config.set({"wgBackendResponseTime":976,"wgHostname":"mw1069"});</script>

In the default HTML output of MediaWiki.

While the latter is a nearly twice as long, it is almost as readable for human
beings, while being substantially easy to get via JavaScript.

To get the values from the comment, you have to do something like:

  var comments, comment, hostname, duration;
  comments = $.grep( document.body.childNodes, function ( el ) {
	return el.nodeType === 8
  } );
  comment = comments.length
	? comments.pop().nodeValue.match( /(\S+) in ([\d.]+)/ ).slice( 1 )
	: [ null, null ];
  hostname = comment[0];
  respTime = parseFloat( comment[1] );

On the other hand, to get the values from the JavaScript code, you can simply:

  var hostname = mw.config.get( 'wgHostname' );
  var respTime = mw.config.get( 'wgBackendResponseTime' );

I believe that the ability to parse the number easily via JavaScript will make
it easier to include with other client-side measurements as part of reports on
site performance as experienced by users.

Change-Id: I895cd03f0968815484ff8cda4b23cc602ac555f0