Tweak layout and label navigation.

kristapsdz · Jul 23, 2018 · 3413693 · 3413693
1 parent 2b42b09
commit 3413693
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 3 deletions.
diff --git a/tools.css b/tools.css
@@ -96,17 +96,18 @@ section + section		{ margin-top: 8rem; }
 				  margin-top: 1rem; }
 
 @media only screen and (max-width: 1280px), only screen and (max-device-width: 1280px) {
-  article, header	{ padding-left: 10%;
+  article, header		{ padding-left: 10%;
 	  			  padding-right: 10%; }
 }
 
 @media only screen and (max-width: 768px), only screen and (max-device-width: 768px) {
   body				{ font-size: 13pt; }
   header			{ padding-top: 4em; }
   header h1			{ font-size: 180%; }
-  article, header	{ padding-left: 2%;
+  article, header		{ padding-left: 2%;
 	  			  padding-right: 2%; }
   .mobile			{ display: block; }
   .desktop			{ display: none; }
+  #last				{ text-align: center; }
 }
 
diff --git a/tools.xml b/tools.xml
@@ -16,7 +16,8 @@
 		<script>
 			function changeEventHandler(event) {
 				if (null !== event.target.value)
-					location.href = '#sec-' + event.target.value;
+					if (event.target.value.length)
+						location.href = '#sec-' + event.target.value;
 			}
 			document.addEventListener('DOMContentLoaded', function() {
 				'use strict';
@@ -63,6 +64,7 @@
 				<div class="mobile">
 					<div class="subnav">
 						<select id="nav-select">
+							<option value="">Jump to&#8230;</option>
 							<option value="c">C</option>
 							<option value="cgi">Fast/CGI</option>
 							<option value="security">Security</option>