/* Time-stamp: <02/12/16 09:37:40 ptr> */
 /* $Id$ */

div.leftfloat {
  float: left;
}

div.rightfloat {
  float: right;
}

div.spacer {
  clear:      both;
}