pre {
  line-height: 110%;
}

.footer {
  background-color: #eee;
}

body > div.container {
  margin-top:10px;
}

dd {
  margin-left: 40px;
}

tt.descname {
  font-size: 100%;
}

code {
  color: rgb(51,51,51);
}

h1 {
  padding-bottom:7px;
  border-bottom: 1px solid #ccc;
}

h2 {
  padding-bottom:5px;
  border-bottom: 1px solid #ccc;
}

h3 {
  padding-bottom:5px;
  border-bottom: 1px solid #ccc;
}

.rubric {
  font-size: 120%;
  padding-bottom:1px;
  border-bottom: 1px solid #ccc;
}

.headerlink {
  padding-left: 1ex;
  padding-right: 1ex;
}

a.headerlink:hover {
  text-decoration: none;
}

blockquote p {
  font-size: 100%;
  font-weight: normal;
  line-height: normal;
};