diff --git a/configure/tools/munch.pl b/configure/tools/munch.pl index 203b7e2eb..9b78d7405 100755 --- a/configure/tools/munch.pl +++ b/configure/tools/munch.pl @@ -13,12 +13,14 @@ while ($line = ) ($adr,$type,$name) = split ' ',$line,3; chop $name; $name =~ s/^__/_/; + next if ( $name =~ /^__?GLOBAL_.D.\.\./ ); @dtorlist = (@dtorlist,$name); }; if ($line =~ /__?GLOBAL_.I.+/) { ($adr,$type,$name) = split ' ',$line,3; chop $name; $name =~ s/^__/_/; + next if ( $name =~ /^__?GLOBAL_.I.\.\./ ); @ctorlist = (@ctorlist,$name); }; }