From: Stefano Zacchiroli Date: Wed, 16 Mar 2005 16:21:44 +0000 (+0000) Subject: user smaller font in result page X-Git-Tag: V_0_6_3_3~4 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6dada2f080978d66e3acc24230eee10e22daabea;p=helm.git user smaller font in result page --- diff --git a/helm/searchEngine/html/moogle_chat.html.src b/helm/searchEngine/html/moogle_chat.html.src index 1e610b744..bda0482d1 100644 --- a/helm/searchEngine/html/moogle_chat.html.src +++ b/helm/searchEngine/html/moogle_chat.html.src @@ -10,7 +10,7 @@ -

Ambiguous input: @EXPRESSION@

diff --git a/helm/searchEngine/html/moogle_header.html.src b/helm/searchEngine/html/moogle_header.html.src index 2100ca24e..d406b0b79 100644 --- a/helm/searchEngine/html/moogle_header.html.src +++ b/helm/searchEngine/html/moogle_header.html.src @@ -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; }