diff options
| author | Luke Dashjr <luke_github1@dashjr.org> | 2020-01-20 05:14:50 +0000 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-01-20 05:14:50 +0000 |
| commit | 6a802329e468b6a5fa24a1f28d2464736e490fbb (patch) | |
| tree | 529171b1d4a33e9a04d325242692c54619975d1c | |
| parent | 24eddbb48a1d686f70bf33172de602d865a244b4 (diff) | |
| parent | 1d20ad8a42a6463dccfc6ca83dfd0aa6bdc01b47 (diff) | |
Merge pull request #877 from kallewoof/linter-http-only
linter: avoid false positives such as C++ lambda exprs by only detect…
| -rwxr-xr-x | scripts/link-format-chk.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/scripts/link-format-chk.sh b/scripts/link-format-chk.sh index 86f28be..e3f0f6d 100755 --- a/scripts/link-format-chk.sh +++ b/scripts/link-format-chk.sh @@ -10,7 +10,7 @@ ECODE=0 FILES="" for fname in $(git diff --name-only HEAD $(git merge-base HEAD master)); do if [[ $fname == *.mediawiki ]]; then - GRES=$(grep -n '](' $fname) + GRES=$(grep -n '](http' $fname) if [ "$GRES" != "" ]; then if [ $ECODE -eq 0 ]; then >&2 echo "Github Mediawiki format writes link as [URL text], not as [text](url):" |