var i = 0;
var chars = ['/', '|', '\\'];
var fan;

function rotate()
{
    if (i > 2)
        i = 0;
    fan.innerHTML = chars[i++];
}

$(document).ready(function ()
{
    fan = document.getElementById('fan');
    if (fan)
        setInterval('rotate();', 300);
/*
    var prettify = false;
    $('pre code').parent().each(function ()
    {
        $(this).addClass('prettyprint');
        prettify = true;
    });
    if (prettify)
        prettyPrint();
*/
})