no message

[creaToolsTools.git] / Linux / menu.sh

diff --git a/Linux/menu.sh b/Linux/menu.sh
index 0b0f976c4f3b378082a5c95186c2eb748faf2d32..3a26fd5d55249aa41eb607761c722ffbea985233 100644 (file)
--- a/Linux/menu.sh
+++ b/Linux/menu.sh
@@ -217,7 +217,7 @@ do
         # ------------------
 
         buildType="___"
-        while [[ "$buildType" != "Release"  && "$Debug " != "HTML" ]]
+        while [[ "$buildType" != "Release"  && "$buildType " != "Debug" ]]
         do
            echo "Build type : Release/Debug (default is Release)"
            read buildType