From 85d47749f968f79bed854a8596ffadb622e22ecc Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 20 Jul 2022 17:12:07 +0200
Subject: [PATCH] [Tools] pre-commit hook moved in ./dev/git-hooks

---
 dev/git-hooks/pre-commit               | 42 --------------------------
 {tools => dev}/git-hooks/pre-commit.sh |  4 +--
 2 files changed, 2 insertions(+), 44 deletions(-)
 delete mode 100755 dev/git-hooks/pre-commit
 rename {tools => dev}/git-hooks/pre-commit.sh (94%)

diff --git a/dev/git-hooks/pre-commit b/dev/git-hooks/pre-commit
deleted file mode 100755
index 36353a8d1a7..00000000000
--- a/dev/git-hooks/pre-commit
+++ /dev/null
@@ -1,42 +0,0 @@
-#!/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
diff --git a/tools/git-hooks/pre-commit.sh b/dev/git-hooks/pre-commit.sh
similarity index 94%
rename from tools/git-hooks/pre-commit.sh
rename to dev/git-hooks/pre-commit.sh
index b48c7b5c22b..14f2d819ae8 100755
--- a/tools/git-hooks/pre-commit.sh
+++ b/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
-- 
GitLab