diff --git a/html/inc/util.inc b/html/inc/util.inc
index 5ac832619d..4a07099bba 100644
--- a/html/inc/util.inc
+++ b/html/inc/util.inc
@@ -450,7 +450,8 @@ function get_int($name, $optional=false) {
 }
 
 function post_int($name, $optional=false) {
-    $x = $_POST[$name];
+    $x = null;
+    if (isset($_POST[$name])) $x = $_POST[$name];
     if (!is_numeric($x)) {
         if ($optional) {
             return null;