diff options
| author | Gibson Fahnestock <gibfahn@gmail.com> | 2017-06-13 16:26:15 +0300 |
|---|---|---|
| committer | Anna Henningsen <anna@addaleax.net> | 2017-06-21 23:43:13 +0300 |
| commit | 18f073f0fed709bad10d1bd03a5b7d7b57a409d3 (patch) | |
| tree | e4945f1fdf211a6779444aea6f05535dc941c139 /Makefile | |
| parent | 5e59c2d21d00e709d87b1e2a65ec84e3d014f762 (diff) | |
build: fail linter if linting not available
PR-URL: https://github.com/nodejs/node/pull/13658
Ref: https://github.com/nodejs/node/pull/13645#issuecomment-308100452
Reviewed-By: João Reis <reis@janeasystems.com>
Reviewed-By: Refael Ackermann <refack@gmail.com>
Reviewed-By: Roman Reiss <me@silverwind.io>
Reviewed-By: James M Snell <jasnell@gmail.com>
Reviewed-By: Colin Ihrig <cjihrig@gmail.com>
Reviewed-By: Tobias Nießen <tniessen@tnie.de>
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -924,6 +924,7 @@ lint: @echo "Linting is not available through the source tarball." @echo "Use the git repo instead:" \ "$ git clone https://github.com/nodejs/node.git" + exit 1 lint-ci: lint endif |