diff options
author | Benjamin Jones <bjones@galois.com> | 2012-10-30 11:48:08 -0700 |
---|---|---|
committer | Benjamin Jones <bjones@galois.com> | 2012-10-30 11:48:08 -0700 |
commit | a5bbb147b8afacedaee3881ea689c9f953f71904 (patch) | |
tree | 414a2cf4b1ed080437d0e2384630f965676e6c1c /doc | |
parent | 37b44115d6ae992dd643fe328e92079bf3e26750 (diff) | |
parent | 7a16129e03a9b369606ec1e7d83870fcf9ea0318 (diff) |
Merge branch 'master' of src.galois.com:/srv/git/FiveUI
Diffstat (limited to 'doc')
-rw-r--r-- | doc/manual_src/style.css | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/manual_src/style.css b/doc/manual_src/style.css index e2e6b0c..aec68f5 100644 --- a/doc/manual_src/style.css +++ b/doc/manual_src/style.css @@ -237,7 +237,7 @@ strong {font-weight: 600;} text-decoration: underline; } -.interior h1.title { +.interior .title { font-size: 5.9375em; font-weight: 600; text-align: center; |