diff options
Diffstat (limited to 'util/pdftexi2dvi')
| -rwxr-xr-x | util/pdftexi2dvi | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/util/pdftexi2dvi b/util/pdftexi2dvi index 62e7c779..f701705f 100755 --- a/util/pdftexi2dvi +++ b/util/pdftexi2dvi @@ -1,5 +1,5 @@ #!/bin/sh -# $Id: pdftexi2dvi,v 1.6 2013/02/16 16:50:28 karl Exp $ +# $Id: texi2pdf 5234 2013-03-12 22:56:31Z karl $ # Written by Thomas Esser. Public domain. # Execute texi2dvi --pdf. @@ -16,7 +16,7 @@ unset RUNNING_BSH # hack around a bug in zsh: test -n "${ZSH_VERSION+set}" && alias -g '${1+"$@"}'='"$@"' -rcs_revision='$Revision: 1.6 $' +rcs_revision='$Revision: 5234 $' rcs_version=`set - $rcs_revision; echo $2` # special-case --version following GNU standards for identifying the @@ -25,7 +25,7 @@ rcs_version=`set - $rcs_revision; echo $2` # obliged to. if test "x$1" = x--version; then cat <<EOF -texi2pdf (GNU Texinfo 5.0) $rcs_version +texi2pdf (GNU Texinfo 5.1) $rcs_version Copyright (C) 2013 Free Software Foundation, Inc. License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html> |