File tree Expand file tree Collapse file tree 3 files changed +18
-0
lines changed
Expand file tree Collapse file tree 3 files changed +18
-0
lines changed Original file line number Diff line number Diff line change @@ -21,3 +21,4 @@ std-gram.ext
2121tools /sections
2222* .synctex.gz
2323* .synctex *
24+ .check.stamp
Original file line number Diff line number Diff line change @@ -30,3 +30,11 @@ clean-examples:
3030 rm -f $(EXAMPLES )
3131
3232examples : $(EXAMPLES )
33+
34+ .PHONY : check
35+ check : .check.stamp
36+
37+ .check.stamp : ../tools/check-source.sh * .tex
38+ @echo " Running tools/check-source.sh"
39+ @../tools/check-source.sh
40+ @touch $@
Original file line number Diff line number Diff line change 11#! /bin/sh
22git config diff.orderFile .gitorder
33git config diff.c++draft.xfuncname ' \\rSec[0-9]+(\[.*\])\{'
4+
5+ precommit=" $( git rev-parse --git-dir) /hooks/pre-commit"
6+ test -f " $precommit " && exit
7+ cat << EOF > "$precommit "
8+ #!/bin/sh
9+ cd \$ (git rev-parse --show-toplevel)/source
10+ make check
11+ EOF
12+ chmod +x " $precommit "
You can’t perform that action at this time.
0 commit comments