[PHP-DOC] cvs: phpdoc /scripts make-partial.php

[anatoly techtonik]

techtonik               Wed Sep 28 11:47:52 2005 EDT

  Modified files:              
    /phpdoc/scripts     make-partial.php 
  Log:
  * (sync) recover manual.xml.in if the script was terminated unexpectedly
  
http://cvs.php.net/diff.php/phpdoc/scripts/make-partial.php?r1=1.2&r2=1.3&ty=u
Index: phpdoc/scripts/make-partial.php
diff -u phpdoc/scripts/make-partial.php:1.2 phpdoc/scripts/make-partial.php:1.3
--- phpdoc/scripts/make-partial.php:1.2 Tue Sep 13 19:41:19 2005
+++ phpdoc/scripts/make-partial.php     Wed Sep 28 11:47:51 2005
@@ -12,7 +12,7 @@
  *
  * @author    Martin Jansen <[EMAIL PROTECTED]>
  * @copyright 2005 The PEAR Group
- * @version   CVS: $Id: make-partial.php,v 1.2 2005/09/13 23:41:19 techtonik 
Exp $
+ * @version   CVS: $Id: make-partial.php,v 1.3 2005/09/28 15:47:51 techtonik 
Exp $
  */
 
 // NOTE: originally from peardoc:/make-partial.php ;
@@ -33,6 +33,7 @@
 $format = "html";
 $sections = array();
 
+$incflag = false;
 foreach ($args[0] as $arg) {
     if ($arg[0] == "--help") {
         showHelp();
@@ -41,6 +42,14 @@
         $format = $arg[1];
     } elseif ($arg[0] == '--include') {
         $sections[] = $arg[1];
+        $incflag = true;
+    }    
+}
+
+if ($incflag) {
+    // collect other space delimited names as section names
+    foreach ($args[1] as $arg) {
+        $sections[] = $arg;
     }
 }
 
@@ -57,15 +66,18 @@
     }
 }
 
+// recover manual.xml.in if the script was terminated unexpectedly
+restoreFile();
+
+copy("manual.xml.in", "manual.xml.in.partial-backup");
+register_shutdown_function("restoreFile", filemtime("manual.xml.in"));
+
 $file = file("manual.xml.in");
 if (!$file) {
     echo "Error: Unable to read manual.xml.in!";
     exit(1);
 }
 
-copy("manual.xml.in", "manual.xml.in.partial-backup");
-register_shutdown_function("restoreFile", filemtime("manual.xml.in"));
-
 $newFile = "";
 $partStack = array();
 $includePart = true;
@@ -162,14 +174,14 @@
 /**
  * Restores the original manual.xml.in file
  */
-function restoreFile($savedmtime) {
+function restoreFile($savedmtime = null) {
     if (!is_file("manual.xml.in.partial-backup")) {
         return;
     }
 
     unlink("manual.xml.in");
     rename("manual.xml.in.partial-backup", "manual.xml.in");
-    touch("manual.xml.in", $savedmtime);
+    if ($savedmtime) touch("manual.xml.in", $savedmtime);
 }
 
 /**