Declares the function exit_use to behave like use but fail if
errors are detected. It can be used in all Makefiles except Pure, which will
write the exception handler explicitly ("exit" will have been declared
already).
#! /bin/csh
grep "$*" {Pure/Syntax,Pure/Thy}/*ML */*ML */*/*ML