[Tools] pre-commit hook moved in ./dev/git-hooks

dev/git-hooks/pre-commit

-#!/bin/bash
-# -*- mode: 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).            #
-#                                                                        #
-##########################################################################
-
-if git rev-parse --verify HEAD >/dev/null 2>&1
-then
-    against=HEAD
-else
-    # Initial commit: diff against an empty tree object
-    against=4b825dc642cb6eb9a060e54bf8d69288fbee4904
-fi
-
-if git config --get frama-c.makelevel > /dev/null 2>&1 ; then
-  MAKELEVEL=-j$(git config --int --get frama-c.makelevel);
-else
-  MAKELEVEL=-j4;
-fi
-
-MANUAL_ML_FILES=\
-$(git diff-index --name-only --diff-filter d $against | \
-    grep -e '^src/.*\.mli\?$' | tr '\n' ' ') \
-make ${MAKELEVEL} lint

tools/git-hooks/pre-commit.sh → dev/git-hooks/pre-commit.sh

@@ -22,8 +22,8 @@
 ##########################################################################
 
 # Examples of installation of this pre-commit hook (client side):
-# - cp ./tools/git-hooks/pre-commit.sh .git/hooks/pre-commit
-# - (cd .git/hooks/ && ln -s ../../tools/git-hooks/pre-commit.sh pre-commit)
+# - cp ./dev/git-hooks/pre-commit.sh .git/hooks/pre-commit
+# - (cd .git/hooks/ && ln -s ../../dev/git-hooks/pre-commit.sh pre-commit)
 
 # Note:
 # - that checks the unstaged version of the files and these files are