Documentation Source Text

Check-in [582eb4ef8a]
Login

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Close the "Menu" button submenu before leaving the page, in case the user returns to the page using the "Back" button.
Downloads: Tarball | ZIP archive
Timelines: family | ancestors | descendants | both | mobile-friendly
Files: files | file ages | folders
SHA1: 582eb4ef8a09815777fe5a3007ec7d875cb146c3
User & Date: drh 2016-08-31 20:59:28.170
Context
2016-08-31
21:18
Adjustments to the CSS for hyperlink buttons. (check-in: c40376b31c user: drh tags: mobile-friendly)
20:59
Close the "Menu" button submenu before leaving the page, in case the user returns to the page using the "Back" button. (check-in: 582eb4ef8a user: drh tags: mobile-friendly)
20:47
Automatically disable the "Search" menu option if the document does not originate from an HTTP server, since there is no chance of running the CGI script in that case. (check-in: 3de5aaebc8 user: drh tags: mobile-friendly)
Changes
Unified Diff Ignore Whitespace Patch
Changes to document_header.tcl.
︙︙
54
55
56
57
58
59
60


61
62
63
64
65
66
67

        var w = document.getElementById("submenu");
        if( w.style.display=="block" ){
          w.style.display = "none";
        }else{
          w.style.display = "block";
        }
      }



      /* Disable the Search feature if we are not operating from CGI, since */
      /* Search is accomplished using CGI and will not work without it. */
      if( !location.origin.match(/http/) ){
        document.getElementById("search_menubutton").style.display = "none";
      }
      








>
>








54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69

        var w = document.getElementById("submenu");
        if( w.style.display=="block" ){
          w.style.display = "none";
        }else{
          w.style.display = "block";
        }
      }
      function menu_off(){document.getElementById("submenu").style.display="none";}
      window.onbeforeunload = function(e){menu_off();}

      /* Disable the Search feature if we are not operating from CGI, since */
      /* Search is accomplished using CGI and will not work without it. */
      if( !location.origin.match(/http/) ){
        document.getElementById("search_menubutton").style.display = "none";
      }
︙︙