diff --git a/compile.php b/compile.php
index 80b18969..ca9a8f54 100755
--- 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";