voice: If $POOL is not set, use <build-dir>/voice-pool by default

It will _vastly_ speed up repeated voice builds.

The voice pool directory will not be erased by a 'make clean'

Change-Id: Ice58d5c5355abfa5a385dfca749f8063e2ee8622

1 files changed, 3 insertions, 0 deletions

diff --git a/tools/configure b/tools/configure
index 2579a38933..43f02f5643 100755
--- a/tools/configure
+++ b/tools/configure
@@ -1078,6 +1078,9 @@ Win(6)4 crosscompile, (T)est plugins, (O)mit plugins, S(m)all C lib, Logf to Ser
     for thislang in `echo $voicelanguage | sed 's/,/ /g'`; do
       voiceconfig "$thislang"
     done
+    if [ -z "$POOL" ] ; then
+        echo " \$POOL is not set, will use <builddir>/voice-pool by default"
+    fi
   fi
   if [ "yes" = "$use_debug" ]; then
     debug="-DDEBUG"