@font-face {
  font-family: GlassTTYVT220;
  src: local("Glass TTY VT220"), local("Glass TTY VT220 Medium"), url(/font/Glass_TTY_VT220.ttf) format("truetype");
}

html {
  margin-top: 0.25em;
  margin-left: 0.75em;
}

pre, div, input {
  font-size: 20px;
  font-family: GlassTTYVT220;
}

span.noshow {
  display: none;
}

span.notfound {
  text-decoration: blink;
}

a.plain {
  text-decoration: none;
}
a:visited {
  color  : gray
}
input {
  border: none;
  margin: 0;
  padding: 0;
}

input[type=submit] {
  text-decoration: underline;
}

div.find {
  float: right;
  margin: 0;
  padding-top: 0;
  padding-right: 1em;
}