diff options
Diffstat (limited to 'third_party/lua/doc/manual.css')
-rw-r--r-- | third_party/lua/doc/manual.css | 26 |
1 files changed, 0 insertions, 26 deletions
diff --git a/third_party/lua/doc/manual.css b/third_party/lua/doc/manual.css deleted file mode 100644 index 269bd4358e..0000000000 --- a/third_party/lua/doc/manual.css +++ /dev/null @@ -1,26 +0,0 @@ -h3 code { - font-family: inherit ; - font-size: inherit ; -} - -pre, code { - font-size: 12pt ; -} - -span.apii { - float: right ; - font-family: inherit ; - font-style: normal ; - font-size: small ; - color: gray ; -} - -p+h1, ul+h1 { - padding-top: 0.4em ; - padding-bottom: 0.4em ; - padding-left: 24px ; - margin-left: -24px ; - background-color: #E0E0FF ; - border-radius: 8px ; -} - |