533   font-family: sans-serif;

   533   font-family: sans-serif;

   534   font-size: 85%;

   534   font-size: 85%;

   535   margin: 0 .5em 0 .5em;

   535   margin: 0 .5em 0 .5em;

   536 }

   536 }

   537 

   537 

   542 hotspot:after {

   538 hotspot:after {

   543   display: marker;

   539   display: marker;

   544   padding-bottom: .7em;

   540   padding-bottom: .7em;

   545   content: insert-same-after-button(color, #7f7f7f, icon, icon(right-half-disc));

   541   content: insert-same-after-button(color, #7f7f7f, icon, icon(right-half-disc));

   546 }

   542 }