p, pre, div, h1, h2, h3, td  { 
  font-size: 100%;
}

body { 
  background-color: #777; 
}

div.topnav {
  margin-bottom: 1.3ex;
  margin-top: 1.3ex;
}

div.manpage {
  background-color: white;
  padding: 1ex;
  margin-top: 1ex;
}

.topnav a {
  color: #ff4;
  padding: 0.2ex 0.8ex;
  text-decoration: none;
  border: 1px dotted #999;
  margin-right: 0.5ex;
}

.topnav a:hover {
  background-color: #997;
  border: 1px dotted #777;
}

tt, tt b {
  color: #800;
  font-size: 110%;
}

b { 
  color: #444;
}

h2.title {
  font-family: courier, fixed;
  border-bottom: 0.3ex dotted #ddd;
  padding-bottom: 0.3ex;
  padding-left: 0.5ex;
  margin-top: 0em;
  font-size: 180%;
}

div.title { 
  padding-left: 1em;
  margin-left: 0.5ex;
  padding-bottom: 1ex;
  margin-bottom: 1em;
  border-left: 3ex solid #ff6;
}

h3 {
  color: #666;
  font-size: 110%;
  margin-bottom: 0em;
  padding-bottom: 0em;
}

pre.example {
  padding: 1.2ex;
  margin-top: 0.8ex; 
  margin-bottom: 1ex; 
  background: #cf8; 
  margin-top: 0ex; 
  color: black;
  font-weight: normal;
  font-size: 110%;
}

div.footer {
  margin-top: 0.5ex;
  font-size: 90%;
  color: #eee;
  text-align: center;
  width: 100%;
}

div.footer a {
  color: #fff;
  margin: 0ex 1ex;
}

table.index td.right {
  padding-left: 1em;
}

center.footerlogo { 
  margin-top: 3em;
}