From 8fbfe494dcd00d07a690a81e6d92bdcef45f005d Mon Sep 17 00:00:00 2001 From: "john.j.camilleri" Date: Wed, 3 Apr 2013 07:02:53 +0000 Subject: [PATCH] RGL browser: add GF logo, give full name in page title --- lib/doc/browse/index.html | 5 +++-- lib/doc/browse/script.js | 2 +- lib/doc/browse/style.css | 4 ++++ 3 files changed, 8 insertions(+), 3 deletions(-) diff --git a/lib/doc/browse/index.html b/lib/doc/browse/index.html index 4d4eaa832..2fdae6d4b 100644 --- a/lib/doc/browse/index.html +++ b/lib/doc/browse/index.html @@ -12,7 +12,8 @@
-

RGL Source Browser

+ +

GF Resource Grammar Library Source Browser

Help Synopsis...
@@ -97,7 +98,7 @@
diff --git a/lib/doc/browse/script.js b/lib/doc/browse/script.js index edc49fc95..6dc1f39c1 100644 --- a/lib/doc/browse/script.js +++ b/lib/doc/browse/script.js @@ -397,7 +397,7 @@ $(document).ready(function() { }); var recalculateHeights = function() { - var x = 40; // just found empirically + var x = 55; // just found empirically $('body').height( $(window).height()-x); $('.maxheight').each(function(){ var obj = $(this); diff --git a/lib/doc/browse/style.css b/lib/doc/browse/style.css index 41a6e9433..b69e45cbb 100644 --- a/lib/doc/browse/style.css +++ b/lib/doc/browse/style.css @@ -22,6 +22,10 @@ header { background:#f2f2f2; padding:10px; } +header img { + height:2em; + vertical-align:bottom; +} header h1 { margin:0 1em 0 0; font-size:1em;