diff --git a/dev/check-files.sh b/dev/check-files.sh
index b442ae45ad40451440a671be11ec26d47cf7ee1f..5bc87e486f9f75c489d21cf75cf8bef12d43bf57 100755
--- a/dev/check-files.sh
+++ b/dev/check-files.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/bin/bash -eu
##########################################################################
# #
# This file is part of Frama-C. #
@@ -29,7 +29,7 @@ DO_HDRCK="yes"
REFERENCE=
MODE="all"
-while [ "$1" != "" ]
+while [ $# -gt 0 ]
do
case "$1" in
"-h"|"-help"|"--help")
@@ -37,8 +37,8 @@ do
echo "OPTIONS"
echo " -h|-help|--help print this message and exit"
echo " -f|--fix fix files"
- echo " -c|--commit check modified files to be commited only"
- echo " -p|--push check modified files to be pushed only"
+ echo " -c|--commit check modified files to be committed only"
+ echo " -p|--push range check modified files to be pushed only"
echo " --no-headers do not check headers"
echo " --no-lint do not check lint"
exit 0
@@ -48,10 +48,12 @@ do
HDRCK=headers
;;
"-p"|"--push")
- REFERENCE="origin/$(git rev-parse --abbrev-ref HEAD)"
+ shift
+ DIFF_ARG=$1
MODE="push"
;;
"-c"|"--commit")
+ DIFF_ARG=--cached
MODE="commit"
;;
"--no-headers")
@@ -70,53 +72,52 @@ done
if [ "$MODE" = "all" ]; then
if [ $DO_LINT = "yes" ] ; then
- make $LINT || exit 1
+ make $LINT
fi
if [ $DO_HDRCK = "yes" ] ; then
# Don't define HDRCK_EXTRA, that is required by external plugins
- make $HDRCK || exit 1
+ make $HDRCK
fi
else
- STAGED=$(git diff --diff-filter ACMR --name-only --cached $REFERENCE | sort)
- UNSTAGED=$(git diff --diff-filter DMR --name-only | sort)
+ TMP_STAGED=$(mktemp)
+ TMP_UNSTAGED=$(mktemp)
+ TMP_INTER=$(mktemp)
+ TMP_INPUT=$(mktemp)
- if [ "$STAGED" = "" ];
+ cleanup () {
+ rm -f "$TMP_STAGED" "$TMP_UNSTAGED" "$TMP_INPUT" "$TMP_INTER"
+ }
+ trap cleanup exit
+ git diff -z --diff-filter ACMR --name-only $DIFF_ARG | sort -z > "$TMP_STAGED"
+ git diff -z --diff-filter DMR --name-only | sort -z > "$TMP_UNSTAGED"
+
+ if [ ! -s "$TMP_STAGED" ];
then
echo "No staged modification since last $MODE, nothing to do."
exit 0
fi
- if [ "$UNSTAGED" != "" ];
+ if [ -s "$TMP_UNSTAGED" ];
then
- INTER=$(comm -12 <(ls $STAGED) <(ls $UNSTAGED))
-
- if [ "$INTER" != "" ];
+ comm -12 --zero-terminated "$TMP_STAGED" "$TMP_UNSTAGED" > "$TMP_INTER"
+ if [ -s "$TMP_INTER" ];
then
echo "Cannot validate push."
echo "The following staged files have been modified, renamed or deleted."
- for file in $INTER ; do
- echo "- $file"
- done
+ while IFS= read -r -d $'\0' f; do
+ echo "- $f"
+ done < "$TMP_INTER"
exit 1
fi
fi
- STAGED=$(echo $STAGED | tr '\n' ' ')
-
- TMP=$(mktemp)
-
- cleanup () {
- rm -f "$TMP"
- }
- trap cleanup exit
-
- if [ $DO_LINT = "yes" ] ; then
- git check-attr -za $STAGED > "$TMP"
- make $LINT LINTCK_FILES_INPUT="$TMP" || exit 1
+ if [ $DO_LINT = "yes" -a -s "$TMP_STAGED" ] ; then
+ git check-attr -za --stdin < "$TMP_STAGED" > "$TMP_INPUT"
+ make $LINT LINTCK_FILES_INPUT="$TMP_INPUT"
fi
- if [ $DO_HDRCK = "yes" ] ; then
- git check-attr -z header_spec $STAGED > "$TMP"
+ if [ $DO_HDRCK = "yes" -a -s "$TMP_STAGED" ] ; then
+ git check-attr -z header_spec --stdin < "$TMP_STAGED" > "$TMP_INPUT"
# Don't define HDRCK_EXTRA, that is required by external plugins
- make $HDRCK HDRCK_FILES_INPUT="$TMP" || exit 1
+ make $HDRCK HDRCK_FILES_INPUT="$TMP_INPUT"
fi
fi
diff --git a/dev/git-hooks/pre-commit.sh b/dev/git-hooks/pre-commit.sh
index 9225fe93451377bcf64eb87f0bf8892838f87e71..5333e2b62eb19f3179948abe78c40a01bdc03680 100755
--- a/dev/git-hooks/pre-commit.sh
+++ b/dev/git-hooks/pre-commit.sh
@@ -23,8 +23,8 @@
# Example of installation of this pre-commit hook (client side):
# - (cd .git/hooks/ && ln -s ../../dev/git-hooks/pre-commit.sh pre-commit)
-# Note: if you decide to copy the file, the `SCRIPT_DIR` variable must be
-# fixed accordingly.
+
+ROOT=$(git rev-parse --show-toplevel)
echo "Pre-commit Hook..."
@@ -36,5 +36,4 @@ then
exit 0
fi
-SCRIPT_DIR=$(dirname -- "$( readlink -f -- "$0"; )")
-"$SCRIPT_DIR/../check-files.sh" -c || exit 1
+"$ROOT/dev/check-files.sh" -c || exit 1
diff --git a/dev/git-hooks/pre-push.sh b/dev/git-hooks/pre-push.sh
index 2859ac02a2486584c83b00d9082d3be760bba57e..7c42e374e1095dd373906ff8bc922872facffb12 100755
--- a/dev/git-hooks/pre-push.sh
+++ b/dev/git-hooks/pre-push.sh
@@ -21,20 +21,30 @@
# #
##########################################################################
-# Example of installation of this pre-push hook (client side):
-# - (cd .git/hooks/ && ln -s ../../dev/git-hooks/pre-push.sh pre-push)
-# Note: if you decide to copy the file, the `SCRIPT_DIR` variable must be
-# fixed accordingly.
+ROOT=$(git rev-parse --show-toplevel)
echo "Pre-push Hook..."
-STAGED=$(git diff --diff-filter ACMR --name-only --cached origin/$(git rev-parse --abbrev-ref HEAD) | sort)
+empty=$(git hash-object --stdin </dev/null | tr '[0-9a-f]' '0')
-if [ "$STAGED" = "" ];
-then
- echo "No diff since last push, nothing to do"
- exit 0
-fi
+remote=$1
-SCRIPT_DIR=$(dirname -- "$( readlink -f -- "$0"; )")
-"$SCRIPT_DIR/../check-files.sh" -p || exit 1
+while read local_ref local_oid remote_ref remote_oid
+do
+ if test "$local_oid" = "$empty"
+ then
+ # Handle delete
+ :
+ else
+ if test "$remote_oid" = "$empty"
+ then
+ # New branch, examine commits starting
+ # the forking point from master
+ remote_oid=$(git merge-base $local_ref master);
+ fi
+ range="$remote_oid $local_oid";
+ "$ROOT/dev/check-files.sh" -p "$range" || exit 1;
+ fi;
+done
+
+exit 0
diff --git a/tests/misc/with-space.i b/tests/misc/with-space.i
index 5a1eddc52babddf2ba7f1b428715ffaf3db82b9b..12017c6154035a1623793b959f44bbc4c231d754 100644
--- a/tests/misc/with-space.i
+++ b/tests/misc/with-space.i
@@ -2,3 +2,4 @@
LIBS: ../with\ space/module
OPT:
*/
+