Lines Matching full:script

27 This script checks that all generated file are up-to-date. If some aren't, by
51 # check SCRIPT FILENAME[...]
52 # check SCRIPT DIRECTORY
53 # Run SCRIPT and check that it does not modify any of the specified files.
57 # list of files in the directory. Running SCRIPT must not modify any file
62     SCRIPT=$1
85     "$SCRIPT"
87     # Compare the script output to the old files and remove backups
94             echo "'$FILE' was either modified or deleted by '$SCRIPT'"
109             echo "Files were deleted or created by '$SCRIPT'"
121 # the format must be "check SCRIPT FILENAME...". For other source files,