body
{
max-width:1200px;  /* might not be a good idea.  Seems to help on really wide monitors, though */
font-size:100%;
background-color:#F5F5F5;
font-family:Arial,Garuda,Helvetica,sans-serif;   /* Garuda: font for Linux */
padding: 10px 10px 10px 10px;
margin: 0 auto 0 auto;
border: 2px solid #509060;
}


.revisions
{
  font-size:0.6em;
}

ol
{
margin-left:1.5cm;
}

ul
{
margin-left:1.5cm;
}


.blue
{
color:blue;
}

.red
{
color:red;
}

.green
{
color:green;
}

.answer h3
{
color:blue;
}

h1
{
color:darkblue;
text-align:center
}

h2
{
color:darkblue;
}

hr
{
color:darkblue;
}

pre 
{
margin-left:1cm;
font-family:courier,courier-new; 
font-size:90%
}

pre.code
{
margin-left:1cm;
font-family:courier,courier-new; 
font-size:90%;
}

pre.program
{
width:auto;
margin-left:1cm;
margin-right:1cm;
padding:0.5cm;
border-style:double;
border-color:darkblue;
background-color:white;
font-family:courier,courier-new; 
font-size:90%;
}

code
{
font-family:courier,courier-new; 
font-size:110%
}

table 
{
margin-left:1cm;
font-family:arial,sans-serif; 
font-size:90%;
}

table pre
{
margin-left:0.4cm;
margin-right:0.4cm;
}

a:link     { color:blue }
a:visited  { color:brown }
a:active   { color:red }
a:hover    { color:red }