0024366: wok_env.sh - default $PRODUCTS_PATH ignores platform

diff --git a/src/WOKsite/wok_env.sh b/src/WOKsite/wok_env.sh
index d5246a1d9cb6999a3ced23f6a84bf220b977adff..e36f9a9da3823fac56dd48aded3dc05ea2a5dd3c 100644 (file)
--- a/src/WOKsite/wok_env.sh
+++ b/src/WOKsite/wok_env.sh
@@ -71,7 +71,7 @@ fi
 
 # ----- 3rd-parties root -----
 if [ "$PRODUCTS_PATH" == "" ]; then
-  export PRODUCTS_PATH="${WOKHOME}/3rdparty/lin32"
+  export PRODUCTS_PATH="${WOKHOME}/3rdparty/${WOKSTATION}${ARCH}"
 fi
 
 # ----- Setup Environment Variables for WOK -----