/* This css file includes some basic formatting stuff,
   which can easily be overridden by internal stylesheets. */

* {
  margin: 0;
  padding: 0;
  font-size: 12px;
  font-family: 'dejavu sans' arial;
}

body {
  padding: 3px;
}

.header {
  font-size: 16px;
}