Allow the user to override whitespace hook setting in dune.module

This patch makes it possible to bypass installation of the whitespace hook by specifying

VCSETUP_FLAGS="DISABLEWHITESPACEHOOK=1"

in the user's options. If dunecontrol encounters that flag, it will not attempt to install
the hook in any module, uninstall the hook if it has already been installed and output a
warning telling the user that he'll have to take care of whitespace by himself.

[[Imported from SVN: r7471]]

bin/dunecontrol

@@ -320,29 +320,48 @@ run_default_vcsetup() {
   fi
 
   if [ -d .git ]; then
+
     # Read Whitespace-Hook setting from dune.module file
     local SETUPGITHOOK="$($GREP -i "^[$BLANK]*Whitespace-Hook:" dune.module | cut -d ':' -f2 | eval $PARSER_TRIM | tr '[:upper:]' '[:lower:]')"
 
     if [ "x$SETUPGITHOOK" = "xyes" ]; then
       # we have to install the Git whitespace hook
-      if [ ! -e .git/hooks/pre-commit ]; then
-        # there is no hook yet, we can safely install ours
-        echo "--> Installing Git pre-commit hook to enforce whitespace policy"
-        cp -p $PREFIX_DIR/bin/git-whitespace-hook .git/hooks/pre-commit
-      else
-        # there is already a hook, check whether it is our whitespace hook
-        local HOOKTAG="$(head -n 2 .git/hooks/pre-commit | tail -n 1)"
-        if [ "x$HOOKTAG" = "x# dune-git-whitespace-hook" ]; then
-          if [ $PREFIX_DIR/bin/git-whitespace-hook -nt .git/hooks/pre-commit ]; then
-            echo "--> Updating Git pre-commit hook with newer version"
-            cp -p $PREFIX_DIR/bin/git-whitespace-hook .git/hooks/pre-commit
+
+      if [ -n "$DISABLEWHITESPACEHOOK" ] ; then
+        # the user doesn't want the Git whitespace hook - deinstall it if necessary and warn the user
+        echo "WARNING: The current module wants to install the DUNE whitespace hook, but you have disabled the hook in your options!"
+        echo "WARNING: You will have to make sure that your commits don't introduce any trailing whitespace or indentation with tabs!"
+        echo "WARNING: Otherwise, your commits might be rejected when trying to push them to an official repository!"
+
+        if [ -e .git/hooks/pre-commit ]; then
+          # there is a pre-commit hook, check whether it is our whitespace hook
+          local HOOKTAG="$(head -n 2 .git/hooks/pre-commit | tail -n 1)"
+          if [ "x$HOOKTAG" = "x# dune-git-whitespace-hook" ]; then
+            echo "--> Removing DUNE whitespace hook as requested by the user"
+            rm .git/hooks/pre-commit
           fi
+        fi
+      else
+        # standard handling of Git whitespace hook
+        if [ ! -e .git/hooks/pre-commit ]; then
+          # there is no hook yet, we can safely install ours
+          echo "--> Installing Git pre-commit hook to enforce whitespace policy"
+          cp -p $PREFIX_DIR/bin/git-whitespace-hook .git/hooks/pre-commit
         else
-          echo "WARNING: Existing pre-commit hook found!"
-          echo "WARNING: Skipping installation of DUNE whitespace hook!"
-          echo "WARNING: If you want to contribute patches to DUNE, you should make sure to call the whitespace hook"
-          echo "WARNING: (dune-common/bin/git-whitespace-hook) from you custom pre-commit hook, otherwise your commits"
-          echo "WARNING: might contain trailing whitespace and will not apply cleanly to the official repositories!"
+          # there is already a hook, check whether it is our whitespace hook
+          local HOOKTAG="$(head -n 2 .git/hooks/pre-commit | tail -n 1)"
+          if [ "x$HOOKTAG" = "x# dune-git-whitespace-hook" ]; then
+            if [ $PREFIX_DIR/bin/git-whitespace-hook -nt .git/hooks/pre-commit ]; then
+              echo "--> Updating Git pre-commit hook with newer version"
+              cp -p $PREFIX_DIR/bin/git-whitespace-hook .git/hooks/pre-commit
+            fi
+          else
+            echo "WARNING: Existing pre-commit hook found!"
+            echo "WARNING: Skipping installation of DUNE whitespace hook!"
+            echo "WARNING: If you want to contribute patches to DUNE, you should make sure to call the whitespace hook"
+            echo "WARNING: (dune-common/bin/git-whitespace-hook) from you custom pre-commit hook, otherwise your commits"
+            echo "WARNING: might contain trailing whitespace and will not apply cleanly to the official repositories!"
+          fi
         fi
       fi
     fi