From ecea007ac9d1438582e3b8c69ecdb7b7bef77003 Mon Sep 17 00:00:00 2001 From: Ingo Schwarze Date: Tue, 5 Aug 2014 00:42:53 +0000 Subject: Remove the old man.cgi. Running that would not be a responsible thing to do, nowadays. --- man-cgi.css | 13 ------------- 1 file changed, 13 deletions(-) delete mode 100644 man-cgi.css (limited to 'man-cgi.css') diff --git a/man-cgi.css b/man-cgi.css deleted file mode 100644 index 5300267c..00000000 --- a/man-cgi.css +++ /dev/null @@ -1,13 +0,0 @@ -body { font-family: Helvetica, Arial, sans-serif; } -body > div { padding-left: 2em; - padding-top: 1em; } -body > div#mancgi { padding-left: 0em; - padding-top: 0em; } -body > div.results { font-size: smaller; } -#mancgi fieldset { text-align: center; - border: thin solid silver; - border-radius: 1em; - font-size: small; } -#mancgi input[name=expr] { width: 25%; } -.results td.title { vertical-align: top; - padding-right: 1em; } -- cgit v1.2.3