BODY{		background: white;
		color: black }

A:link{         background: white;
                color: blue }
A:visited{	background: white;
		color: rgb(50%, 0%, 50%) }

H1{		background: white;
		color: rgb(55%, 55%, 55%);
		font-family: monospace;
		font-size: x-large;
		text-align: center }

H2{		background: white;
		color: rgb(40%, 40%, 40%);
		font-family: monospace;
		font-size: large;
		text-align: center }

H3{		background: white;
		color: rgb(40%, 40%, 40%);
		font-family: monospace;
		font-size: large }

H4{		background: white;
		color: rgb(40%, 40%, 40%);
		font-family: monospace;
		font-style: italic;
		font-size: large }

H5{		background: white;
		color: rgb(40%, 40%, 40%);
		font-family: monospace }

H6{		background: white;
		color: rgb(40%, 40%, 40%);
		font-family: monospace;
		font-style: italic }
		
IMG.toplogo{	vertical-align: middle }

IMG.arrow{	width: 30px;
		height: 30px;
		border: 0 }

span.acronym{font-size: small}
span.env{font-family: monospace}
span.file{font-family: monospace}
span.option{font-family: monospace}
span.pkg{font-weight: bold}
span.samp{font-family: monospace}

div.vignettes a:hover {
  background: rgb(85%, 85%, 85%);
}