diff --git a/js/src/functions.js b/js/src/functions.js
index ce9532f20c..e42f853d03 100644
--- a/js/src/functions.js
+++ b/js/src/functions.js
@@ -103,6 +103,20 @@ $.ajaxPrefilter(function (options, originalOptions) {
     }
 });
 
+/**
+ * Get an empty string for user-agent, if undefined
+ *
+ * @return {string}
+ */
+Functions.userAgent = function () {
+    try {
+        return navigator.userAgent;
+    } catch (e) {
+        console.error(e);
+        return '';
+    }
+};
+
 /**
  * Adds a date/time picker to an element
  *
@@ -1095,7 +1109,7 @@ AJAX.registerOnload('functions.js', function () {
     /**
      * Add attribute to text boxes for iOS devices (based on bugID: 3508912)
      */
-    if (navigator.userAgent.match(/(iphone|ipod|ipad)/i)) {
+    if (Functions.userAgent().match(/(iphone|ipod|ipad)/i)) {
         $('input[type=text]').attr('autocapitalize', 'off').attr('autocorrect', 'off');
     }
 });
diff --git a/js/src/makegrid.js b/js/src/makegrid.js
index 54bef74551..74dd32680a 100644
--- a/js/src/makegrid.js
+++ b/js/src/makegrid.js
@@ -260,7 +260,7 @@ var makeGrid = function (t, enableResize, enableReorder, enableVisib, enableGrid
             for (var n = 0, l = $firstRowCols.length; n < l; n++) {
                 var $col = $($firstRowCols[n]);
                 var colWidth;
-                if (navigator.userAgent.toLowerCase().indexOf('safari') !== -1) {
+                if (Functions.userAgent().toLowerCase().indexOf('safari') !== -1) {
                     colWidth = $col.outerWidth();
                 } else {
                     colWidth = $col.outerWidth(true);
@@ -2317,10 +2317,10 @@ var makeGrid = function (t, enableResize, enableReorder, enableVisib, enableGrid
     $.fn.noSelect = function (p) { // no select plugin by Paulo P.Marinas
         var prevent = (p === null) ? true : p;
         /* eslint-disable compat/compat */
-        var isMsie = navigator.userAgent.indexOf('MSIE') > -1 || !!window.navigator.userAgent.match(/Trident.*rv:11\./);
-        var isFirefox = navigator.userAgent.indexOf('Firefox') > -1;
-        var isSafari = navigator.userAgent.indexOf('Safari') > -1;
-        var isOpera = navigator.userAgent.indexOf('Presto') > -1;
+        var isMsie = Functions.userAgent().indexOf('MSIE') > -1 || !!Functions.userAgent().match(/Trident.*rv:11\./);
+        var isFirefox = Functions.userAgent().indexOf('Firefox') > -1;
+        var isSafari = Functions.userAgent().indexOf('Safari') > -1;
+        var isOpera = Functions.userAgent().indexOf('Presto') > -1;
         /* eslint-enable compat/compat */
         if (prevent) {
             return this.each(function () {
diff --git a/libraries/classes/Header.php b/libraries/classes/Header.php
index 7916094469..558ad289c1 100644
--- a/libraries/classes/Header.php
+++ b/libraries/classes/Header.php
@@ -334,7 +334,8 @@ class Header
 
         // The user preferences have been merged at this point
         // so we can conditionally add CodeMirror, other scripts and settings
-        if ($GLOBALS['cfg']['CodemirrorEnable']) {
+        // See #20159, why we need to check for HTTP_USER_AGENT here
+        if ($GLOBALS['cfg']['CodemirrorEnable'] && isset($_SERVER['HTTP_USER_AGENT'])) {
             $this->scripts->addFile('vendor/codemirror/lib/codemirror.js');
             $this->scripts->addFile('vendor/codemirror/mode/sql/sql.js');
             $this->scripts->addFile('vendor/codemirror/addon/runmode/runmode.js');