diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/build-system.txt | 4 | ||||
| -rwxr-xr-x | dev/lint-commits.sh | 19 |
2 files changed, 16 insertions, 7 deletions
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index 1c4fd2eba4..fd3101613a 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -143,7 +143,9 @@ file list(s): These files are also used by the experimental ocamlbuild plugin, which is quite touchy about them : be careful with order, duplicated entries, whitespace errors, and do not mention .mli there. - - For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget) + If module B depends on module A, then B should be after A in the .mllib + file. +- For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget) - The definitions in Makefile.common might have to be adapted too. - If your file needs a specific rule, add it to Makefile.build diff --git a/dev/lint-commits.sh b/dev/lint-commits.sh index eb12bc2273..d8043558eb 100755 --- a/dev/lint-commits.sh +++ b/dev/lint-commits.sh @@ -19,14 +19,21 @@ fi BASE_COMMIT="$1" HEAD_COMMIT="$2" -# git diff --check -# uses .gitattributes to know what to check -if git diff --check "$BASE_COMMIT" "$HEAD_COMMIT"; +bad=() +while IFS= read -r commit; do + echo Checking "$commit" + # git diff --check + # uses .gitattributes to know what to check + if ! git diff --check "${commit}^" "$commit"; + then + bad+=("$commit") + fi +done < <(git rev-list "$HEAD_COMMIT" --not "$BASE_COMMIT" --) + +if [ "${#bad[@]}" != 0 ] then - : -else >&2 echo "Whitespace errors!" - >&2 echo "Running 'git diff --check $BASE_COMMIT $HEAD_COMMIT'." + >&2 echo "In commits ${bad[*]}" >&2 echo "If you use emacs, you can prevent this kind of error from reocurring by installing ws-butler and enabling ws-butler-convert-leading-tabs-or-spaces." exit 1 fi |