diff options
Diffstat (limited to 'util/texi2pdf')
-rwxr-xr-x | util/texi2pdf | 21 |
1 files changed, 20 insertions, 1 deletions
diff --git a/util/texi2pdf b/util/texi2pdf index a030a74..11eadc8 100755 --- a/util/texi2pdf +++ b/util/texi2pdf @@ -1,5 +1,5 @@ #!/bin/sh -# $Id: texi2pdf,v 1.2 2005/01/28 01:52:04 karl Exp $ +# $Id: texi2pdf 5381 2013-09-26 23:03:58Z karl $ # Written by Thomas Esser. Public domain. # Execute texi2dvi --pdf. @@ -16,4 +16,23 @@ unset RUNNING_BSH # hack around a bug in zsh: test -n "${ZSH_VERSION+set}" && alias -g '${1+"$@"}'='"$@"' +rcs_revision='$Revision: 5381 $' +rcs_version=`set - $rcs_revision; echo $2` + +# special-case --version following GNU standards for identifying the +# program name. If --version is specified as other than the first +# argument, we don't output the standard name, but then, we're not +# obliged to. +if test "x$1" = x--version; then + cat <<EOF +texi2pdf (GNU Texinfo 5.2) $rcs_version + +Copyright (C) 2013 Free Software Foundation, Inc. +License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html> +This is free software: you are free to change and redistribute it. +There is NO WARRANTY, to the extent permitted by law. +EOF + exit 0 +fi + texi2dvi --pdf ${1+"$@"} |