Fix a PHP warning about "Undefined index"

We must keep track of the nohistory parameter between each call of
display.php.

diff --git a/display.php b/display.php
index 242d45c5e3f02d84d9bcd374018a3f6859051091..eccb64b111a3d15b606e2bbc24f45d79fd8aca84 100644 (file)
--- a/display.php
+++ b/display.php
@@ -514,6 +514,7 @@
                if (isset($_REQUEST['table'])) $_gets['table'] = $_REQUEST['table'];
                if (isset($_REQUEST['sortkey'])) $_gets['sortkey'] = $_REQUEST['sortkey'];
                if (isset($_REQUEST['sortdir'])) $_gets['sortdir'] = $_REQUEST['sortdir'];
+               if (isset($_REQUEST['nohistory'])) $_gets['nohistory'] = $_REQUEST['nohistory'];
                $_gets['strings'] = $_REQUEST['strings'];
 
                if ($save_history && is_object($rs) && ($type == 'QUERY')) //{