/** Hide an html element given its id */
function hideElementById(id)
{
    // hide the element by setting css attribute
    document.getElementById(id).style.display = 'none'
}

// Show the subversion revision number in the page title
function showRevision()
{
    var title = document.title;
    title = title + revisionNumber;
    document.title = title;
}