tests are now handled with a standard Makefile that does not use do_tests.sh

[helm.git] / helm / www / matita / style.css

diff --git a/helm/www/matita/style.css b/helm/www/matita/style.css
index a5898e43f3aafbeef1e299ac6c206eb724db3dd3..64cc6d8b494b7f439b837f745f892101db7cb2ee 100644 (file)
--- a/helm/www/matita/style.css
+++ b/helm/www/matita/style.css
@@ -7,6 +7,10 @@ body {
   margin-right: 7%;
 }
 
+samp.tiny {
+  font-size: 8pt;
+}
+
 span.h1 {
   font-family: sans-serif;
   font-size: 16pt;