File fix_name_git_hook.patch of Package dune-common

Overview Repositories Revisions Requests Users Attributes Meta

File fix_name_git_hook.patch of Package dune-common (Revision eb303822d9e0ce82be78ac8facdc4fb0)

Currently displaying revision eb303822d9e0ce82be78ac8facdc4fb0 , Show latest

From b5da76ba8586e7f67704408dc5ecb3637349c930 Mon Sep 17 00:00:00 2001
From: Ansgar Burchardt <ansgar.burchardt@tu-dresden.de>
Date: Sun, 17 Nov 2019 01:17:49 +0100
Subject: [PATCH 1/2] Rename git-whitespace-hook to dune-git-whitespace-hook.

The name git-whitespace-hook is a bit too generic for a DUNE-specific
tool.
---
 bin/dunecontrol | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

diff --git a/bin/dunecontrol b/bin/dunecontrol
index 1d107799..6b6254d5 100755
--- a/bin/dunecontrol
+++ b/bin/dunecontrol
@@ -521,17 +521,28 @@ run_default_vcsetup() {
         fi
       else
         # standard handling of Git whitespace hook
+        for f in dune-git-whitespace-hook git-whitespace-hook; do
+          f="${PREFIX_DIR}/bin/${f}"
+          if [ -e "${f}" ]; then
+            git_whitespace_hook="${f}"
+            break
+          fi
+        done
+        if [ -z "${git_whitespace_hook:-}" ]; then
+          echo "Did not find git-whitespace-hook." >&2
+          exit 1
+        fi
         if [ ! -e "$GITHOOKPATH" ]; 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" "$GITHOOKPATH"
+          cp -p "${git_whitespace_hook}" "$GITHOOKPATH"
         else
           # there is already a hook, check whether it is our whitespace hook
           local HOOKTAG="$(eval head -n 2 \"$GITHOOKPATH\" | tail -n 1)"
           if [ "x$HOOKTAG" = "x# dune-git-whitespace-hook" ]; then
-            if [ "$PREFIX_DIR/bin/git-whitespace-hook" -nt "$GITHOOKPATH" ]; then
+            if [ "${git_whitespace_hook}" -nt "$GITHOOKPATH" ]; then
               echo "--> Updating Git pre-commit hook with newer version"
-              cp -p "$PREFIX_DIR/bin/git-whitespace-hook" "$GITHOOKPATH"
+              cp -p "${git_whitespace_hook}" "$GITHOOKPATH"
             fi
           else
             echo "WARNING: Existing pre-commit hook found!"
-- 
2.16.4

Places

File fix_name_git_hook.patch of Package dune-common (Revision eb303822d9e0ce82be78ac8facdc4fb0)

Places