]> matita.cs.unibo.it Git - helm.git/commitdiff
user smaller font in result page
authorStefano Zacchiroli <zack@upsilon.cc>
Wed, 16 Mar 2005 16:21:44 +0000 (16:21 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Wed, 16 Mar 2005 16:21:44 +0000 (16:21 +0000)
helm/searchEngine/html/moogle_chat.html.src
helm/searchEngine/html/moogle_header.html.src

index 1e610b74407612185a0945c2d18ecc4afa932f0d..bda0482d189ca3f47daea223ea4f69aaee9ea2b6 100644 (file)
@@ -10,7 +10,7 @@
   <body>
     <helm:include href="moogle_form.html.src" />
     <helm:include href="moogle_querybar.html.src" />
-    <div>
+    <div style="font-size: larger;">
       <p>
        <b>Ambiguous input:</b> <kbd>@EXPRESSION@</kbd>
       </p>
index 2100ca24ecdbe3c29b646a461e166fb02950519f..d406b0b79225d46c569e37edfdc1e9be581a7e2e 100644 (file)
@@ -35,6 +35,7 @@
     b.query_kind { font-size: large }
     body {
       font-family: sans-serif;
+      font-size: smaller;
       background-color: #ffffff;
     }
     span.uri { color: blue; }