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