From 067c8ba353237b7dcce81553397cf366a945f997 Mon Sep 17 00:00:00 2001 From: Martin Beaudoin Date: Sat, 8 Apr 2017 20:22:24 +0000 Subject: [PATCH] ThirdParty: flex. Suggest using FLEX_DIR for a system-installed flex located at a non-traditionnal directory like /opt --- etc/prefs.sh-EXAMPLE | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/etc/prefs.sh-EXAMPLE b/etc/prefs.sh-EXAMPLE index c8c0e0de0..4b70b3aa0 100644 --- a/etc/prefs.sh-EXAMPLE +++ b/etc/prefs.sh-EXAMPLE @@ -160,8 +160,10 @@ export FOAM_VERBOSE=1 # System installed bison #export BISON_SYSTEM=1 -# System installed flex +# System installed flex. FLEX_DIR should point to the directory where +# $FLEX_DIR/bin/flex is located #export FLEX_SYSTEM=1 +#export FLEX_DIR=/usr # System installed m4 #export M4_SYSTEM=1