lib/scripts/unsymbolize
changeset 41457 3bb2f035203f
parent 35022 c844b93dd147
child 52617 42e02ddd1568
equal deleted inserted replaced
41456:006d85ad56d3 41457:3bb2f035203f
    44     s/\\?\\<leftharpoondown>/<=/g;
    44     s/\\?\\<leftharpoondown>/<=/g;
    45 
    45 
    46     my $result = $_;
    46     my $result = $_;
    47 
    47 
    48     if ($text ne $result) {
    48     if ($text ne $result) {
    49 	print STDERR "fixing $file\n";
    49         print STDERR "fixing $file\n";
    50         if (! -f "$file~~") {
    50         if (! -f "$file~~") {
    51 	    rename $file, "$file~~" || die $!;
    51             rename $file, "$file~~" || die $!;
    52         }
    52         }
    53 	open (FILE, "> $file") || die $!;
    53         open (FILE, "> $file") || die $!;
    54 	print FILE $result;
    54         print FILE $result;
    55 	close FILE || die $!;
    55         close FILE || die $!;
    56     }
    56     }
    57 }
    57 }
    58 
    58 
    59 
    59 
    60 ## main
    60 ## main