website: get rid of home-made autoreload in favor of new livereload feature in jekyll 3.7

.gitignore

@@ -15,9 +15,6 @@ nohup.out
 
 build
 /_*
-/docs/lab/_serve*
-/docs/lab/fonts
-/docs/_site
 /githash.txt
 
 /src/FontInspector.html

docs/.gitignore

@@ -0,0 +1,3 @@
+/.jekyll-metadata
+/_site
+/lab/fonts

docs/_includes/autoreload-in-debug.html

@@ -1,46 +0,0 @@
-{% if site.safe == false %}
-<!-- During authoring, this automatically reloads the post as its changing -->
-<script type="text/javascript">
-(function() {
-var qs = document.location.search;
-var current_etag = qs.match(/etag=("?[a-zA-Z0-9_-]+)/);
-if (current_etag !== null) { current_etag = current_etag[1]; }
-var scrolly = qs.match(/scrolly=([0-9]+)/);
-if (scrolly) {
-  scrolly = parseInt(scrolly[1]);
-  if (scrolly > 0) {
-    window.scrollTo(window.scrollX, scrolly);
-    setTimeout(function () {
-      window.scrollTo(window.scrollX, scrolly);
-    }, 10);
-  }
-}
-
-function check() {
-  var r = new XMLHttpRequest();
-  var url = document.location.href + ((qs && qs !== '') ? '&' : '?') + 'r=' + Math.random();
-  r.open('GET', url, true);
-  r.onreadystatechange = function() {
-    if (r.readyState == 4){
-      var found_etag = r.getResponseHeader('Etag');
-      if (found_etag) {
-        found_etag = found_etag.replace(/^"|"$/g);
-      }
-      //console.log('current_etag:', current_etag, 'found_etag:', found_etag);
-      if (current_etag === null) {
-        current_etag = found_etag;
-      } else if (found_etag && found_etag !== current_etag) {
-        document.location.search =
-          '?etag=' + encodeURIComponent(found_etag) +
-          '&scrolly=' + window.scrollY;
-        return;
-      }
-      setTimeout(check, 500);
-    }
-  };
-  r.send(null);
-}
-check();
-})();
-</script>
-{% endif %}

docs/_layouts/default.html

@@ -96,6 +96,5 @@ endfor
       gtag('config', 'UA-105091131-2');
     </script>
     {% endif %}
-    {% include autoreload-in-debug.html %}
   </body>
 </html>

docs/_scripts/serve.sh

@@ -25,4 +25,9 @@ if [ "$1" != "" ]; then
   BINDADDR=$1
 fi
 
-jekyll serve --limit_posts 20 --watch --host "$BINDADDR" --port 3002
+jekyll serve \
+  --incremental \
+  --watch \
+  --host "$BINDADDR" \
+  --port 3002 \
+  --livereload