Don't ask for Doc generation

diff --git a/Linux/menu.sh b/Linux/menu.sh
index aa640b080355618ab8f9d9bcb4783c8da8fa30ab..1423a7594f7fbb82180bb73835a289b4d6611491 100644 (file)
--- a/Linux/menu.sh
+++ b/Linux/menu.sh
@@ -189,6 +189,8 @@ do
         echo 
         # ------------------
 
+if [ false ]
+then
         docgeneration="___"
         while [[ "$docgeneration" != "ON"  && "$docgeneration" != "OFF" ]]
         do
@@ -202,6 +204,9 @@ do
         done
         echo
         echo
+fi
+docgeneration="OFF"
+
         # ------------------
 
         sourcesFrom="___"