.REFBODY {
  margin-bottom: 20px;
}
.REFBODY+p {
  margin-top: 30px;
  margin-bottom: 5px;
}
.function-name {
  font-family: $monoFont;
  display: block;
  margin: 0;
  min-height: none;
  font-weight: bold;
}