lib/Tools/nonascii
author wenzelm
Wed Nov 22 21:41:39 2000 +0100 (2000-11-22)
changeset 10511 efb3428c9879
parent 9788 df671fa2562a
child 10555 2323ec838401
permissions -rwxr-xr-x
tuned;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 # Author: Markus Wenzel, TU Muenchen
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     6 #
     7 # DESCRIPTION: check files for non-ASCII characters
     8 
     9 
    10 ## diagnostics
    11 
    12 PRG="$(basename "$0")"
    13 
    14 function usage()
    15 {
    16   echo
    17   echo "Usage: $PRG [FILES|DIRS...]"
    18   echo
    19   echo "  Recursively find .thy/.ML files and check for non-ASCII characters."
    20   echo
    21   exit 1
    22 }
    23 
    24 
    25 ## process command line
    26 
    27 [ "$#" -eq 0 -o "$1" = "-?" ] && usage
    28 
    29 SPECS="$@"; shift "$#"
    30 
    31 
    32 ## main
    33 
    34 #set by configure
    35 AUTO_PERL=perl
    36 
    37 find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \
    38   xargs "$AUTO_PERL" -w -e \
    39     'while(<ARGV>) { if (m/[\x80-\xff]/) { print "$ARGV: $_"; }}'