body {
	font-family: Courier New;
	font-size: 13px;
	color: #BBBBBB;
	background-color: #000000;
}
 
a:link, a:active, a:visited, a:hover {
	text-decoration: none;
	color: #00FF00;
}
 
.keyword {
	color: #FF0;
}
 
.mirror_links a {
	text-decoration: none;
	color: #00FF00;
}
.mirror_links {
	margin-left: 30px;
}
 
 
/*h1#file_header {
	font-size: 1em;
	margin-bottom: 0px;
}*/
 
.file_links {
	/*margin-left: 20px;*/
}
.file_links h2 {
	font-size: 1em;
	margin-bottom: 0.2em;
}