www/jm.css

   1 div.mirror-navigator {
   2         text-align: right;
   3         font-size: small;
   4 }
   5
   6 div.copyright {
   7         text-align: right;
   8         font-family: Helvetica, Arial, sans-serif;
   9         font-size: smaller;
  10         color: rgb(40%,40%,40%)
  11 }
  12
  13 div.obsolete {
  14     padding: 2px 5px 2px 5px;
  15     margin-right: 5px;
  16     margin-top: 5px;
  17     margin-bottom: 18px;
  18     position: fixed;
  19     top: 1px;
  20     right: 0px;
  21     width: 25em;
  22     font-size: 75%;
  23     color: #b94a48;
  24     background-color: #f2dede;
  25     border-color: #eed3d7;
  26     border-radius: 4px;
  27     border: 1px solid #fbefd5;
  28 }
  29
  30 div#googlesearch {
  31     width: 30em;
  32 }
  33
  34 /* for narrower devices */
  35 @media (max-width:30em) {
  36         div#googlesearch { width: 100%;}
  37 }
  38
  39 body {
  40         background: lightcyan; /* BEIGE; */
  41         color: black;
  42         margin-left: 3%;
  43         margin-right: 3%;
  44 }
  45
  46 h1 {
  47         background-color: powderblue;
  48         text-align: center;
  49         border-style: inset;
  50         border-width: 0 3 3 0;
  51         border-color: #000;
  52 }
  53
  54 h2 {
  55         background-color: powderblue;
  56         border-style: inset;
  57         border-width: 0 2 2 0;
  58         border-color: #000;
  59 }
  60
  61 h3 {
  62         background-color: powderblue;
  63         border-width: 0 0 1 0;
  64         border-color: #000;
  65 }
  66
  67 p {
  68         text-indent: 0em;
  69 }
  70
  71 p.indent {
  72         text-indent: 1em;
  73 }
  74
  75 p.noindent {
  76         text-indent: 0em;
  77 }
  78
  79 strong {
  80         font-weight: bold;
  81 }
  82
  83 dl dd {
  84         padding-top: 0.3em;
  85         padding-bottom: 0.3em;
  86 }
  87
  88 ul li {
  89         padding-bottom: 0.3em;
  90 }
  91
  92 pre {
  93         padding: 0.3em;
  94         background: #dddddd;
  95 }
  96
  97 .gsc-control-cse {
  98         background-color: lightcyan !important;
  99         border: 0em !important;
 100         padding: 0em !important;
 101 }
 102
 103 /* 'man on WWW' form */
 104         table.searchbox {
 105                 max-width:100%;
 106                 margin: 1em 2%;
 107         }
 108
 109         table.searchbox th {
 110                 text-align: left;
 111                 vertical-align: top;
 112                 word-break: keep-all;
 113                 font-weight: bold;
 114                 font-family: sans-serif;
 115         }
 116
 117         input[name="Pagename"] { width:30em; }
 118         @media (max-width:30em) {
 119                 input[name="Pagename"] { width:100%; }
 120         }
 121
 122 /* Local configs for browsing locally downloaded files */
 123 @import url(local.css)
 124
 125 /* EOF */