Index: auto/options
===================================================================
--- auto/options	(revision e4cec26b9f4157c18cc9809b9570c3f2eb14cc03)
+++ auto/options	(revision 9a367616612b9e69c7e0bb155d5b543d50824483)
@@ -25,4 +25,8 @@
 if [ -z "$CP" ];                then CP=$DEFAULT_CP;                                fi
 if [ -z "$CHMOD" ];             then CHMOD=$DEFAULT_CHMOD;                          fi
+if [ -z "$MAKEINFO" ];          then MAKEINFO=$DEFAULT_MAKEINFO;                    fi
+if [ -z "$TEXI2DVI" ];          then TEXI2DVI=$DEFAULT_TEXI2DVI;                    fi
+if [ -z "$TEXI2PDF" ];          then TEXI2PDF=$DEFAULT_TEXI2PDF;                    fi
+if [ -z "$DVIPS" ];             then DVIPS=$DEFAULT_DVIPS;                          fi
 
 if [ -z "$CFLAGS" ];            then CFLAGS=$DEFAULT_CFLAGS;                        fi
@@ -80,4 +84,9 @@
     CP=*)               CP="$value"                               ;;
     CHMOD=*)            CHMOD="$value"                            ;;
+    MAKEINFO=*)         MAKEINFO="$value"                         ;;
+    TEXI2DVI=*)         TEXI2DVI="$value"                         ;;
+    TEXI2PDF=*)         TEXI2PDF="$value"                         ;;
+    DVIPS=*)            DVIPS="$value"                            ;;
+
 
     CFLAGS=*)           CFLAGS="$value"                           ;;
@@ -136,4 +145,9 @@
   CP                    cp command
   CHMOD                 chmod command
+  MAKEINFO              makeinfo command
+  TEXI2DVI              texi2dvi command
+  TEXI2PDF              texi2pdf command
+  DVIPS                 dvips command
+
 
   CFLAGS                C compiler flags