window.onload = function()
{
	var element = document.getElementsByTagName("pre");
	for (i=0; i<element.length; i++)
	{
		element[i].className += " prettyprint";
	}
	if (element.length > 0) prettyPrint();
}