RGL browser: add GF logo, give full name in page title

This commit is contained in:
john.j.camilleri
2013-04-03 07:02:53 +00:00
parent 56a299df79
commit 8fbfe494dc
3 changed files with 8 additions and 3 deletions

View File

@@ -12,7 +12,8 @@
</head>
<body>
<header>
<h1>RGL Source Browser</h1>
<img src="../../../doc/Logos/gf0.png" alt="" />
<h1 title="...or GFRGLSB as we like to call it">GF Resource Grammar Library Source Browser</h1>
<a class="tab help" href="#help">Help</a>
<a href="http://www.grammaticalframework.org/lib/doc/synopsis.html" target="_blank">Synopsis...</a>
</header>
@@ -97,7 +98,7 @@
<br style="clear:both" />
</div>
<footer id="footer">
John J. Camilleri<br/><em>Updated 2013-01-29</em>
John J. Camilleri<br/><em>Updated 2013-04-03</em>
</footer>
<script src="http://ajax.googleapis.com/ajax/libs/jquery/1.7.2/jquery.min.js"></script>
<script src="jquery.history.min.js"></script>

View File

@@ -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);

View File

@@ -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;