Show a different tagline for print media

The taglines are a little fun thing to have, but in printouts, they
cannot change all the time, so let's have a fixed one there.

Signed-off-by: Johannes Schindelin <[email protected]>

Author: dscho

assets/js/application.js

@@ -37,6 +37,7 @@ $(document).ready(function() {
   Downloads.init();
   DownloadBox.init();
   PostelizeAnchor.init();
+  Print.init();
 });
 
 function onPopState(fn) {
@@ -808,6 +809,27 @@ var Graphviz = {
   }
 }
 
+var Print = {
+  init: function() {
+    Print.tagline = $("#tagline");
+    Print.scrollToTop = $("#scrollToTop");
+    window.matchMedia("print").addListener((mediaQueryList) => {
+      Print.toggle(mediaQueryList.matches);
+    });
+  },
+  toggle: function(enable) {
+    if (enable) {
+      Print.taglineBackup = Print.tagline.html();
+      Print.tagline.html("--print-out");
+      Print.scrollToTopDisplay = Print.scrollToTop.attr("display");
+      Print.scrollToTop.attr("display", "none");
+    } else {
+      Print.tagline.html(Print.taglineBackup || "--as-git-as-it-gets");
+      Print.scrollToTop.attr("display", Print.scrollToTopDisplay);
+    }
+  }
+}
+
 // Scroll to Top
 $('#scrollToTop').removeClass('no-js');
 $(window).on('scroll', function() {