From f3ca6de1eb2d1899ed6fa2cc1b5d2edd245471a9 Mon Sep 17 00:00:00 2001 From: "Dylan K. Taylor" Date: Fri, 2 Sep 2022 20:00:52 +0100 Subject: [PATCH] shut --- src/Server.php | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Server.php b/src/Server.php index ac22f74b5..88888445b 100644 --- a/src/Server.php +++ b/src/Server.php @@ -132,6 +132,7 @@ use function get_class; use function ini_set; use function is_array; use function is_dir; +use function is_int; use function is_object; use function is_resource; use function is_string;