<html><head><meta name="color-scheme" content="light dark"></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">/* layout.css
 *
 * Layout settings which are used by all pages in the site.
 *
 * This file was copied and modified from www.wiggy.net, and was
 * written by Wichert Akkerman (c) 2002, 2003
 *
 */

body {
	color:			black;
	background: 		white;
	padding:		0;
	margin-left:		0;
}

div.main {

	margin-right:		2.5em;
	margin-left:		14.5em;
	margin-bottom:		2em;
	padding:		0 .5em .5em;
/*	background:		rgb(226,255,244); */
}


div.smallmain {
	border:			1px solid black;
	margin-right:		14.5em;
	margin-left:		14.5em;
	margin-bottom:		2em;
	padding:		0 .5em .5em;
/*	background:		rgb(226,255,244); */
}

div.copyright {
	font-size:		smaller;
	color:			black;

	border:			none;
	float: 			bottom;
	margin-bottom:		1em;
	clear:			both;
	text-align: right;

}

h3 {
	text-align: center;
}


div.nav {
	float:			left;
	clear:			both;
	margin-left:		1em;
	border:			1px solid black;
	border-collapse:	collapse;
	width:			12em;
	background:		rgb(230,230,230);
}

div.nav ul {
	list-style-position:	outside;
	margin-left:		1em;
	padding-left:		1em;
}


div.nav ul ul {
	padding-left:		0;
}


div.nav li.closedfolder {
	list-style-image:	url("https://www.gnu.org/css/folder-closed.gif");
}


div.nav li.openfolder {
	list-style-image:	url("https://www.gnu.org/css/folder-open.gif");
}


div.nav li.item {
	list-style:		disc;
}


div.nav a {
	text-decoration:	none;
}


div.nav a:hover {
/*	background:	rgb(69,232,177); */
}


div.news {
	position:		relative;
	float:			right;
	clear:			both;
	margin-left:		1em;
	margin-right:		1em;
	border:			1px solid black;
	border-collapse:	collapse;
	width:			12em;
	background:		rgb(230,230,230);
}


table.overview {
	text-align:	left;
}

table.overview th {
	text-align:	left;
	vertical-align:	top;
}


pre.example {
	overflow:	auto;
	background:	rgb(230,230,230);
	border:		solid;
	border-width:	thin;
}

pre.code {
	overflow:	auto;
	padding:	1em;
	border:		solid;
	border-width:	thin;
	background:	rgb(230, 230, 230);
}

span.command {
	font-family:	monospace;
}

dt {
	font-weight:	bold;
}
</pre></body></html>