Support compiling Elastic driver

diff --git a/compile.php b/compile.php
index 80b18969123c33801d8392ec9f482257c4cd6792..ca9a8f54a2c647e86b9e0bd2075e581de4be0b9e 100755 (executable)
--- a/compile.php
+++ b/compile.php
@@ -371,6 +371,10 @@ function number_type() {
        return '';
 }
 
+function ini_bool() {
+       return true;
+}
+
 $project = "adminer";
 if ($_SERVER["argv"][1] == "editor") {
        $project = "editor";