/* Time-stamp: <05/11/04 22:04:46 ptr> */
 /* $Id$ */

.nodecor a:link {
  text-decoration: none;
  color: #666666;
}

.nodecor a:visited {
  text-decoration: none;
  color: #7f7f7f;
}

.nodecor a.nodecor:active {
  text-decoration: none;
  color: black;
}

.nodecor a:hover {
  text-decoration: none;
  color: #868686;
}

div.warning {
  border:  1px solid red;
  /* color:   red; */
  padding-left: 2em;
  padding-right: 2em;
}

:target {
  border: 2px solid red;
}