NOMINUM_PUBLIC_DELETE will cause an entire file to be deleted.

diff --git a/util/sanitize.pl b/util/sanitize.pl
index 41b999f46f6c78cc23b526ea6452d1c4c3113445..28ae7007529b37e7edeee3adef989511e8b605c0 100644 (file)
--- a/util/sanitize.pl
+++ b/util/sanitize.pl
@@ -15,7 +15,7 @@
 # NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION
 # WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 
-# $Id: sanitize.pl,v 1.4 2000/08/19 01:02:07 gson Exp $
+# $Id: sanitize.pl,v 1.5 2000/09/26 22:44:19 bwelling Exp $
 
 # Don't try and sanitize this file: NOMINUM_IGNORE
 
@@ -34,6 +34,8 @@
 # in the file, and a warning is generated, unless the string
 # NOMINUM_IGNORE appears before NOMINUM_PUBLIC.
 
+# If the string NOMINUM_PUBLIC_DELETE is present, delete the file.
+
 # Usage:
 #  ./sanitize.pl -c   - Check syntax only, don't change anything
 #  ./sanitize.pl -i   - Reverse sense of sanitize.
@@ -86,7 +88,14 @@ sub runfile($) {
                        unlink($_[1]);
                        break;
                }
-               if (/\#ifdef.+NOMINUM_PUBLIC/) {
+               elsif (/NOMINUM_PUBLIC_DELETE/) {
+                       close(INFILE);
+                       close(OUTFILE);
+                       unlink($_[0]);
+                       unlink($_[1]);
+                       break;
+               }
+               elsif (/\#ifdef.+NOMINUM_PUBLIC/) {
                        if ($state != 0) {
                                print(STDERR "*** ERROR in file $_[0]".
                                      "line $.: ".