@font-face {
  font-family: DejaVuSansMono;
  src: local("DejaVu Sans Mono"),
       url(fonts/DejaVuSansMono.ttf);
}

@font-face {
  font-family: DejaVuSansMono;
  src: local("DejaVu Sans Mono Bold"),
       url(fonts/DejaVuSansMono-Bold.ttf);
  font-weight: bold;
}

body {
  text-align: center;
  font-family: DejaVuSansMono;
  /* Disable font boosting */
  -webkit-text-size-adjust: none;
  -moz-text-size-adjust: none;
  -ms-text-size-adjust: none;
}

h4 {
  text-align: left;
  margin: auto;
  width: 720px;
}

p {
  text-align: left;
  margin: auto;
  width: 720px;
  line-height: 24px;
  margin-top: 1em;
  margin-bottom: 1em;
}

pre {
  font-family: DejaVuSansMono;
}

input {
  display: block;
  margin: auto;
  margin-top: 1em;
  margin-bottom: 1em;
}