Commit 2b701fcd authored by Heiko Becker's avatar Heiko Becker

Fix pre-commit hook and forward HOL4 and cakeML

parent 4730f8a8
Subproject commit ffce1e98edd43af5f177e1c1cdb612e8c4ac7f29
Subproject commit 7f486a5f00f273d5ba21cc8ea98aaddf822ec371
#!/bin/sh
#!/bin/bash
# Check that the HOLCOMMIT variable and the HOL commit coincide:
HOLCOMMIT_LOCAL="$(cat ./hol4/.HOLCOMMIT)"
pushd
DIR=`pwd`
FLOVERDIR=${DIR/FloVer\/*/FloVer\/}
HOLCOMMIT_LOCAL="$(cat $FLOVERDIR/hol4/.HOLCOMMIT)"
cd $HOLDIR
HOLCOMMIT_GLOBAL="$(git rev-parse HEAD)"
popd
cd $DIR
if [["$HOLCOMMIT_LOCAL" = "HOLCOMMIT_GLOBAL"]]
if [[ "$HOLCOMMIT_LOCAL" = "$HOLCOMMIT_GLOBAL" ]]
then
exit 0
else
......@@ -17,52 +20,5 @@ else
that your changes either compile with the state specified in
./hol4/.HOLCOMMIT or update the file.
EOF
exit 1
#
# An example hook script to verify what is about to be committed.
# Called by "git commit" with no arguments. The hook should
# exit with non-zero status after issuing an appropriate message if
# it wants to stop the commit.
#
# To enable this hook, rename this file to "pre-commit".
# 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 you want to allow non-ASCII filenames set this variable to true.
#allownonascii=$(git config --bool hooks.allownonascii)
# Redirect output to stderr.
#exec 1>&2
# Cross platform projects tend to avoid non-ASCII filenames; prevent
# them from being added to the repository. We exploit the fact that the
# printable range starts at the space character and ends with tilde.
#if [ "$allownonascii" != "true" ] &&
# Note that the use of brackets around a tr range is ok here, (it's
# even required, for portability to Solaris 10's /usr/bin/tr), since
# the square bracket bytes happen to fall in the designated range.
# test $(git diff --cached --name-only --diff-filter=A -z $against |
# LC_ALL=C tr -d '[ -~]\0' | wc -c) != 0
#then
# cat <<\EOF
#Error: Attempt to add a non-ASCII file name.
#
#This can cause problems if you want to work with people on other platforms.
#
#To be portable it is advisable to rename the file.
#
#If you know what you are doing you can disable this check using:
#
# git config hooks.allownonascii true
#EOF
# exit 1
#fi
# If there are whitespace errors, print the offending file names and fail.
#exec git diff-index --check --cached $against --
exit 1
fi
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment