# $Id: texi,v 5.1 2012/08/30 16:29:12 ksb Exp $
#  Verify that the file is a TexInfo file

$*(*): if %~/bin/is-texinfo %f\n\tthen\n\t\t%b %o -m%m -d%s -e'%~/is/texinfo%%;' %f\n\telse\n\t\t%${echo-echo} "%f: is not a TexInfo file" && ${false-false}\n\tfi

$*(*): if %~/bin/is-texinfo %f\n\tthen\n\t\t%b %o -m%m -e'%~/is/texinfo%%;' %f\n\telse\n\t\t%${echo-echo} "%f: is not a TexInfo file" && ${false-false}\n\tfi