Index: auto/options
===================================================================
--- auto/options	(revision 63a5739817f03a720db39f375f3d3c53646fba4c)
+++ auto/options	(revision 44f59b8b510ac7c3b21f669b0d25ed4cb4201f3f)
@@ -14,4 +14,5 @@
 if [ -z "$CC" ];                then CC=$DEFAULT_CC;                                fi
 if [ -z "$BISON" ];             then BISON=$DEFAULT_BISON;                          fi
+if [ -z "$FLEX" ];              then FLEX=$DEFAULT_FLEX;                            fi
 if [ -z "$RM" ];                then RM=$DEFAULT_RM;                                fi
 if [ -z "$RMDIR" ];             then RMDIR=$DEFAULT_RMDIR;                          fi
@@ -65,4 +66,5 @@
     CC=*)               CC="$value"                               ;;
     BISON=*)            BISON="$value"                            ;;
+    FLEX=*)             FLEX="$value"                             ;;
     RM=*)               RM="$value"                               ;;
     RMDIR=*)            RMDIR="$value"                            ;;