diff --git a/bin/dunecontrol b/bin/dunecontrol index 9db2d5ee505b73662e9607e4666f15b812d4a970..cf894c5552971ad02a50e5fdb478d8574d449643 100755 --- a/bin/dunecontrol +++ b/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