From bd48373d2eb918b6713d4958970238b10026c100 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Date: Fri, 4 Jun 2021 16:47:59 +0200
Subject: [PATCH] Adapting the pre-commit script (sanity-git.sh) to
 pactole-dev.

Reminder: to make it active, you need to do the following each time
you clone pactole-dev (assuming you do NOT already have a pre-commit
script in .git/hooks):

cp sanity-git.sh .git/hooks/pre-commit
chmod u+x .git/hooks/pre-commit
---
 sanity-git.sh | 21 ++++++++++++++++-----
 1 file changed, 16 insertions(+), 5 deletions(-)

diff --git a/sanity-git.sh b/sanity-git.sh
index 6032a19a..c6d79027 100755
--- a/sanity-git.sh
+++ b/sanity-git.sh
@@ -1,7 +1,20 @@
 #!/bin/sh
 
-# if launched by git commit
-# cd dev_coq
+# This script checks that pactole archive is in a correct state:
+# - no coq file should be there but not cited in _CoqProject (untrackedvfiles).
+# - no file cited in _CoqProject should be absent (unfoundvfiles).
+#
+# NOTE: we do note check that compilation succeeds. It is too long and
+# should be checked by CI anyway..
+
+# To enable this as a pre-commit check, do (assuming you do NOT
+# already have a pre-commit script in .git/hooks):
+#
+# cp sanity-git.sh .git/hooks/pre-commit
+# chmod u+x .git/hooks/pre-commit
+#
+# Note that you will need to do that on each local clone you have, as
+# it is not versionized.
 
 AUXFILES=".allvfiles .trackedfiles .untrackedvfiles .unfoundvfiles"
 
@@ -54,6 +67,7 @@ NC='\033[0m' # No Color
 if [ "$EXITCODE2" -eq 1 -a "$EXITCODE1" -eq 1 ];
 then
     EXITCODE=0
+    echo "Sanity check OK"
 else
     echo "${RED}Commit was aborted for the reason described above.${NC}"
     echo
@@ -67,7 +81,4 @@ fi
 
 rm -f $AUXFILES
 
-# if launched by git commit
-# cd ..
-
 exit $EXITCODE
-- 
GitLab