<!--
   function title()
   {
      var path = window.location.pathname;
      var tilda = path.indexOf('~');
      if (-1 != tilda) {
         path = path.slice(tilda+1);
      }
      else {
         var unicode = path.indexOf('%7E');
         if (-1 != unicode)
            path = path.slice(unicode+3);
      }
      path = path.slice(0,path.lastIndexOf('/'));
      if (path != 'nkraft') {
         path = path.replace(/\//g,'.');
         document.title = path;
      }
   }
// -->