1 files changed, 20 insertions, 1 deletions
diff --git a/util/pdftexi2dvi b/util/pdftexi2dvi
index 17708e7..11eadc8 100755
--- a/util/pdftexi2dvi
+++ b/util/pdftexi2dvi
@@ -1,5 +1,5 @@
 #!/bin/sh
-# $Id: pdftexi2dvi,v 1.3 2007/07/05 15:22:26 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+"$@"}