Skip files in .gitignore in check-typo

2019-03-07 11:52:13 +00:00 · 2019-03-07 11:52:13 +00:00 · 3f91e8750b
parent db215dda8f
commit 3f91e8750b
1 changed files with 1 additions and 0 deletions
--- a/tools/check-typo
+++ b/tools/check-typo
@ -171,6 +171,7 @@ EXIT_CODE=0
 ) | (
  while read f; do
    if test -n "$(check_prune "$f")"; then continue; fi
+    if $(git check-ignore -q "$f"); then continue; fi
    case `$OCAML_CT_LS_FILES "$f" 2>&1` in
      "") path_in_index=false;;
      *) path_in_index=true;;