more font size tweaks.

diff --git a/webcit-ng/static/js/main.js b/webcit-ng/static/js/main.js
index d40131e11b92046426ff8562601e3d2cd8367ce5..150caae267534e9d5f5a5656d143422ee755b5e9 100644 (file)
--- a/webcit-ng/static/js/main.js
+++ b/webcit-ng/static/js/main.js
@@ -16,7 +16,7 @@ do_biff = async() => {
        }
 
        if (new_mail > 0) {
-               console.log("YOU'VE GOT MAIL!");
+               console.log("YOU'VE GOT MAIL!  new_mail = " + new_mail);
                new_mail_sound.play();                  // FIXME do a visual notification as well
                new_mail = 0;
        }