body {
	font-size: 13px;
/*	margin-top: 0px; */
}

div.menu {
	text-align: center;
	margin-top: 12px;
	margin-bottom: 3px;
	background: #eeeeff;
	font-variant: small-caps;
/*	position: fixed;*/
	width: 100%;
}
div.menu a {
	text-decoration: none;
	color: #0020a0;
}
div.menu hr.menu {
	height: 4px;
	background: #fe0;
	border: 0px;
	margin-top: 0px;
	margin-bottom: 0px;
}

div.title {
	font: bold normal 2em sans-serif ;
	margin: 0px;
	color: #0020a0;
}

h1 {
	font: bold normal 1.7em sans-serif ;
	margin: 0px;
	color: #0020a0;
}
h1.sub {
	font: bold normal 1.3em sans-serif ;
	text-align: right ;
	color: #0020a0;
}
h1 a {
	color: #0020a0;
	text-decoration: none;
}

h2 {
	font: bold normal small-caps 1.3em sans-serif ;
	color: #0020a0;
	margin-top: 8px;
	margin-bottom: 8px;
}

h4 {
	font: bold normal small-caps 1em sans-serif ;
	color: #0020a0;
	margin-top: 8px;
	margin-bottom: 4px;
}

h6.mirrors {
	text-align: right;
	margin: 0px;
	font-size: 10px;
}

div.section {
	background: #eeeeff;
	padding-left: 2px;
	padding-bottom: 2px;
	margin-top: 12px;
	margin-bottom: 12px;
}

p {
	margin-top: 8px;
	margin-bottom: 4px;
	margin-left: 6px;
	margin-right: 6px;
}

hr {
	height: 8px;
	background: #fe0;
	border: 0px;
	margin-top: 6px;
	margin-bottom: 6px;
}

pre {
	font-size: 12px;
	background: #dddddd;
	padding: 3px;
	padding-left: 0px;
	margin-left: 12px;
}

a {
	font-weight: bold;
}

div.publis-desc {
	text-align: right;
	font-style: italic;
	font-size: 12px;
	padding-left: 15%;
}

p.updated {
	text-align: right;
	font-size: 10px;
	font-style: italic;
}

div.line {
        font-family: monospace, fixed;
        font-size: 13px;
        min-height: 13px;
        line-height: 1.0;
        text-wrap: unrestricted;
        white-space: -moz-pre-wrap; /* Moz */
        white-space: -pre-wrap;     /* Opera 4-6 */
        white-space: -o-pre-wrap;   /* Opera 7 */
        white-space: pre-wrap;      /* CSS3  */
        word-wrap: break-word;      /* IE 5.5+ */
        text-indent: -53px;
        padding-left: 53px;
        padding-bottom: 0px;
        margin: 0px;
        -webkit-transition-property: background-color, box-shadow;
        -webkit-transition-duration: 0.5s;
        -moz-transition-property: background-color, box-shadow;
        -moz-transition-duration: 0.5s;
        -ms-transition-property: background-color, box-shadow;
        -ms-transition-duration: 0.5s;
        -o-transition-property: background-color, box-shadow;
        -o-transition-duration: 0.5s;
        transition-property: background-color, box-shadow;
        transition-duration: 0.5s;
}

div.line.glow {
        background-color: cyan;
        box-shadow: 0 0 10px cyan;
}