Some additional sanity.

diff --git a/win32/installer/setini.php b/win32/installer/setini.php
index c16ea02f98a8fc56eadaa368aede4e7c6040f0ed..cdcb65fc07b85827b114fd60f1c082ce5811b5fe 100644 (file)
--- a/win32/installer/setini.php
+++ b/win32/installer/setini.php
@@ -11,14 +11,32 @@
 
 echo "Running post-installation script to configure php.ini\n";
 
+function fatal($msg)
+{
+       echo $msg;
+       sleep(5);
+       exit(1);
+}
+
 $ini_name = $argv[1];
 $option_file = $argv[2];
 
+if (!file_exists($option_file)) {
+       fatal("Option file $option_file does not exist");
+}
+
+if (!file_exists($ini_name)) {
+       fatal("inifile $ini_name does not exist");
+}
+
 $options = explode("\n", file_get_contents($option_file));
 $opts = array();
 
 /* Parse the options */
 foreach ($options as $line) {
+       if (strlen(trim($line)) == 0)
+               continue;
+
        list($name, $value) = explode("=", $line);
 
        if ($name == "extension") {
@@ -48,6 +66,7 @@ foreach ($lines as $line) {
                extract($optdata);
                
                if (preg_match($pat, $line)) {
+                       echo "Found $pat ; setting $name to $value\n";
                        $line = "$name=$value\r\n";
                        // No need to match again
                        unset($opts[$k]);
@@ -64,5 +83,5 @@ unlink($ini_name);
 rename($new_name, $ini_name);
 
 echo "All done!\n";
-
+sleep(1);
 ?>