diff options
Diffstat (limited to 'doc/fptools.css')
-rw-r--r-- | doc/fptools.css | 36 |
1 files changed, 0 insertions, 36 deletions
diff --git a/doc/fptools.css b/doc/fptools.css deleted file mode 100644 index 5c7fc47b..00000000 --- a/doc/fptools.css +++ /dev/null @@ -1,36 +0,0 @@ -div { - font-family: sans-serif; - color: black; - background: white -} - -h1, h2, h3, h4, h5, h6, p.title { color: #005A9C } - -h1 { font: 170% sans-serif } -h2 { font: 140% sans-serif } -h3 { font: 120% sans-serif } -h4 { font: bold 100% sans-serif } -h5 { font: italic 100% sans-serif } -h6 { font: small-caps 100% sans-serif } - -pre { - font-family: monospace; - border-width: 1px; - border-style: solid; - padding: 0.3em -} - -pre.screen { color: #006400 } -pre.programlisting { color: maroon } - -div.example { - background-color: #fffcf5; - margin: 1ex 0em; - border: solid #412e25 1px; - padding: 0ex 0.4em -} - -a:link { color: #0000C8 } -a:hover { background: #FFFFA8 } -a:active { color: #D00000 } -a:visited { color: #680098 } |