back to latest head

[mir.git] / web / produced / style / mir.css

diff --git a/web/produced/style/mir.css b/web/produced/style/mir.css
deleted file mode 100755 (executable)
index 6c12b85..0000000
--- a/web/produced/style/mir.css
+++ /dev/null
@@ -1,5 +0,0 @@
-a {  color: #0000CC; text-decoration: underline}
-a:hover {  color: #333333; text-decoration: none}
-td {  font-family: "Times New Roman", Times, serif}
-.small {  font-size: x-small}
-pre {  font-family: "Courier", Courier, serif}