File tree Expand file tree Collapse file tree 3 files changed +23
-0
lines changed Expand file tree Collapse file tree 3 files changed +23
-0
lines changed Original file line number Diff line number Diff line change @@ -21,3 +21,4 @@ std-gram.ext
21
21
tools /sections
22
22
* .synctex.gz
23
23
* .synctex *
24
+ .check.stamp
Original file line number Diff line number Diff line change @@ -30,3 +30,12 @@ clean-examples:
30
30
rm -f $(EXAMPLES )
31
31
32
32
examples : $(EXAMPLES )
33
+
34
+ check : .check.stamp
35
+
36
+ .check.stamp : ../tools/check-source.sh * .tex
37
+ @echo " Running tools/check-source.sh"
38
+ @../tools/check-source.sh
39
+ @touch $@
40
+
41
+ .PHONY : default refresh refresh full quiet clean-figures figures clean-examples examples check
Original file line number Diff line number Diff line change 1
1
#! /bin/sh
2
2
git config diff.orderFile .gitorder
3
3
git config diff.c++draft.xfuncname ' \\rSec[0-9]+(\[.*\])\{'
4
+
5
+ precommit=" $( git rev-parse --git-dir) /hooks/pre-commit"
6
+
7
+ test -f " ${precommit} " && exit
8
+ read -p " Install 'make check' pre-commit hook? [Y/n] " hook
9
+ if [ -z " ${hook} " -o " ${hook} " = " y" -o " ${hook} " = " Y" ]; then
10
+ cat << EOF > "${precommit} "
11
+ #!/bin/sh
12
+ cd \$ (git rev-parse --show-toplevel)/source
13
+ make check
14
+ EOF
15
+ chmod +x " ${precommit} "
16
+ fi
You can’t perform that action at this time.
0 commit comments