Improve JavaScript

Avoid an error reported by TypeScript 4.1.5 (`href` might be undefined).

_javascripts_src/page.ts:6:34 - error TS2345: Argument of type
'string | undefined' is not assignable to parameter of type 'string'.
Type 'undefined' is not assignable to type 'string'.

6    if (current_page.indexOf($(this).attr('href')) == 0) {
                              ~~~~~~~~~~~~~~~~~~~~

Author: stomar

_javascripts_src/page.ts

@@ -3,7 +3,8 @@ var Page = {
         highlight: function () {
             var current_page = location.pathname;
             $("#header div.site-links a:not(.home)").each(function (i) {
-                if (current_page.indexOf($(this).attr('href')) == 0) {
+                let element_href = $(this).attr('href');
+                if (element_href && current_page.indexOf(element_href) == 0) {
                     $(this).addClass('selected');
                 }
             });

javascripts/page.js

@@ -4,7 +4,8 @@ var Page = {
         highlight: function () {
             var current_page = location.pathname;
             $("#header div.site-links a:not(.home)").each(function (i) {
-                if (current_page.indexOf($(this).attr('href')) == 0) {
+                var element_href = $(this).attr('href');
+                if (element_href && current_page.indexOf(element_href) == 0) {
                     $(this).addClass('selected');
                 }
             });