diff options
Diffstat (limited to 'tools/configure')
-rwxr-xr-x | tools/configure | 3 |
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 | |||
1078 | for thislang in `echo $voicelanguage | sed 's/,/ /g'`; do | 1078 | for thislang in `echo $voicelanguage | sed 's/,/ /g'`; do |
1079 | voiceconfig "$thislang" | 1079 | voiceconfig "$thislang" |
1080 | done | 1080 | done |
1081 | if [ -z "$POOL" ] ; then | ||
1082 | echo " \$POOL is not set, will use <builddir>/voice-pool by default" | ||
1083 | fi | ||
1081 | fi | 1084 | fi |
1082 | if [ "yes" = "$use_debug" ]; then | 1085 | if [ "yes" = "$use_debug" ]; then |
1083 | debug="-DDEBUG" | 1086 | debug="-DDEBUG" |