From a60c2adffa112ae053a9de1b7ed7cd5791fdc74c Mon Sep 17 00:00:00 2001
From: jean-pierre roux <jean-pierre.roux@creatis.insa-lyon.fr>
Date: Mon, 9 May 2011 12:43:23 +0000
Subject: [PATCH] Don't ask for Doc generation

---
 Linux/menu.sh | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/Linux/menu.sh b/Linux/menu.sh
index aa640b0..1423a75 100644
--- 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="___"
-- 
2.45.1