/**
 * Input: $Date: 2002/05/14 11:09:08 $
 * Output: 30-Apr-2002
 */
function formatCvsDate(dateStr)
{
	// var dateStr = "$Date: 2002/05/14 11:09:08 $";
	
	var day = dateStr.slice(15, 17);
	var monthNum = Number(dateStr.slice(12, 14));
	var year = dateStr.slice(7, 11);
	
	var months = new Array("undefined", "Jan", "Feb", "Mar", "Apr", "May", "Jun", "Jul", "Aug", "Sep", "Oct", "Nov", "Dec");
	var monthStr = months[monthNum];
	
	return day + "-" + monthStr + "-" + year;
}


/**
 * Input: $Id: functions.js,v 1.2 2002/05/14 11:09:08 adam Exp $
 * Output: footer.html
 */
function extractCvsFileName(idStr)
{
	// var idStr = "$Id: functions.js,v 1.2 2002/05/14 11:09:08 adam Exp $";
	
	var rightPos = idStr.indexOf(",");
	return idStr.slice(5, rightPos);
}