diff --git a/dev/check-files.sh b/dev/check-files.sh
new file mode 100755
index 0000000000000000000000000000000000000000..60cb4899acf926f7457a17a351b32eb3506d4a19
--- /dev/null
+++ b/dev/check-files.sh
@@ -0,0 +1,120 @@
+#!/bin/bash
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2022 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+THIS_SCRIPT="$0"
+LINT=check-lint
+HDRCK=check-headers
+DO_LINT="yes"
+DO_HDRCK="yes"
+REFERENCE=
+MODE="all"
+
+while [ "$1" != "" ]
+do
+ case "$1" in
+ "-h"|"-help"|"--help")
+ echo "${THIS_SCRIPT} [OPTIONS]"
+ 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 " --no-headers do not check headers"
+ echo " --no-lint do not check lint"
+ exit 0
+ ;;
+ "-f"|"--fix")
+ LINT=lint
+ HDRCK=headers
+ ;;
+ "-p"|"--push")
+ REFERENCE="origin/$(git rev-parse --abbrev-ref HEAD)"
+ MODE="push"
+ ;;
+ "-c"|"--commit")
+ MODE="commit"
+ ;;
+ "--no-headers")
+ DO_HDRCK="no"
+ ;;
+ "--no-lint")
+ DO_LINT="no"
+ ;;
+ *)
+ echo "Unknown option '$1'"
+ exit 2
+ ;;
+ esac
+ shift
+done
+
+if [ "$MODE" = "all" ]; then
+ if [ $DO_LINT = "yes" ] ; then
+ make $LINT || exit 1
+ fi
+ if [ $DO_HDRCK = "yes" ] ; then
+ make $HDRCK HDRCK_EXTRA="-quiet" || exit 1
+ fi
+else
+ STAGED=$(git diff --diff-filter ACMR --name-only --cached $REFERENCE | sort)
+ UNSTAGED=$(git diff --diff-filter DMR --name-only | sort)
+
+ if [ "$STAGED" = "" ];
+ then
+ echo "No staged modification since last $MODE, nothing to do."
+ exit 0
+ fi
+
+ if [ "$UNSTAGED" != "" ];
+ then
+ INTER=$(comm -12 <(ls $STAGED) <(ls $UNSTAGED))
+
+ if [ "$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
+ exit 1
+ fi
+ fi
+
+ STAGED=$(echo $STAGED | tr '\n' ' ')
+
+ TMP=$(mktemp)
+
+ cleanup () {
+ rm "$TMP"
+ }
+ trap cleanup exit
+
+ git check-attr -za $STAGED > "$TMP"
+ if [ $DO_LINT = "yes" ] ; then
+ make $LINT LINTCK_FILES_INPUT="$TMP" || exit 1
+ fi
+ git check-attr -z header_spec $STAGED > "$TMP"
+ if [ $DO_HDRCK = "yes" ] ; then
+ make $HDRCK HDRCK_FILES_INPUT="$TMP" HDRCK_EXTRA="-quiet" || exit 1
+ fi
+fi
diff --git a/dev/git-hooks/pre-commit.sh b/dev/git-hooks/pre-commit.sh
index 05a1af918e1b2aa27c94cfe9608b8c176c8e8040..0f460288e035b37a0005579ac86f16db4524ea5f 100755
--- a/dev/git-hooks/pre-commit.sh
+++ b/dev/git-hooks/pre-commit.sh
@@ -21,14 +21,14 @@
# #
##########################################################################
-# Examples of installation of this pre-commit hook (client side):
-# - cp ./dev/git-hooks/pre-commit.sh .git/hooks/pre-commit
+# 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.
echo "Pre-commit Hook..."
STAGED=$(git diff --diff-filter ACMR --name-only --cached | sort)
-UNSTAGED=$(git diff --diff-filter DMR --name-only | sort)
if [ "$STAGED" = "" ];
then
@@ -36,31 +36,5 @@ then
exit 0
fi
-if [ "$UNSTAGED" != "" ];
-then
- INTER=$(comm -12 <(ls $STAGED) <(ls $UNSTAGED))
-
- if [ "$INTER" != "" ];
- then
- echo "Cannot validate commit."
- echo "The following staged files have been modified, renamed or deleted."
- for file in $INTER ; do
- echo "- $file"
- done
- exit 1
- fi
-fi
-
-STAGED=$(echo $STAGED | tr '\n' ' ')
-
-TMP=$(mktemp)
-
-cleanup () {
- rm "$TMP"
-}
-trap cleanup exit
-
-git check-attr -za $STAGED > "$TMP"
-make lint LINTCK_FILES_INPUT="$TMP" || exit 1
-git check-attr -z header_spec $STAGED > "$TMP"
-make check-headers HDRCK_FILES_INPUT="$TMP" HDRCK_EXTRA="-quiet" || exit 1
+SCRIPT_DIR=$(dirname -- "$( readlink -f -- "$0"; )")
+"$SCRIPT_DIR/../check-files.sh" -c || exit 1
diff --git a/dev/git-hooks/pre-push.sh b/dev/git-hooks/pre-push.sh
index 4521eb81400b22a2f7699d21ee63409d56e4188e..d06723672d1f370c970b72816d144b073419231d 100755
--- a/dev/git-hooks/pre-push.sh
+++ b/dev/git-hooks/pre-push.sh
@@ -21,14 +21,14 @@
# #
##########################################################################
-# Examples of installation of this pre-push hook (client side):
-# - cp ./dev/git-hooks/pre-push.sh .git/hooks/pre-push
+# 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.
echo "Pre-push Hook..."
STAGED=$(git diff --diff-filter ACMR --name-only --cached origin/$(git rev-parse --abbrev-ref HEAD) | sort)
-UNSTAGED=$(git diff --diff-filter DMR --name-only | sort)
if [ "$STAGED" = "" ];
then
@@ -36,31 +36,5 @@ then
exit 0
fi
-if [ "$UNSTAGED" != "" ];
-then
- INTER=$(comm -12 <(ls $STAGED) <(ls $UNSTAGED))
-
- if [ "$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
- exit 1
- fi
-fi
-
-STAGED=$(echo $STAGED | tr '\n' ' ')
-
-TMP=$(mktemp)
-
-cleanup () {
- rm "$TMP"
-}
-trap cleanup exit
-
-git check-attr -za $STAGED > "$TMP"
-make lint LINTCK_FILES_INPUT="$TMP" || exit 1
-git check-attr -z header_spec $STAGED > "$TMP"
-make check-headers HDRCK_FILES_INPUT="$TMP" HDRCK_EXTRA="-quiet" || exit 1
+SCRIPT_DIR=$(dirname -- "$( readlink -f -- "$0"; )")
+"$SCRIPT_DIR/../check-files.sh" -p || exit 1