Bugfix/lint infrastructure improvements #648
Conversation
|
Looks good to me, but I'd suggest @thk123 and @jgwilson42 to be the reviewers of this one. |
scripts/cpplint.py
Outdated
There was a problem hiding this comment.
How come this break is required?
There was a problem hiding this comment.
Because we want to find the git repository immediately containing the working directory, not the one closest to root. Otherwise this doesn't match up with the folder used by the git diff.
|
@forejtv, please have a look why the Linter is unhappy with the new "ignoring" output. |
|
@tautschnig can we get this merged now? |
|
With @NathanJPhillips's help, I have a fix for the linter: Change https://github.com/diffblue/cbmc/blob/master/scripts/run_lint.sh#L65 to |
|
@NathanJPhillips, can you apply this fix please? Then we can merge |
NathanJPhillips
changed the title
NathanJPhillips
force-pushed
the
bugfix/lint-work-across-repos
branch
from
e4cf395 to
2175b3d
Compare
Made linter use paths relative to current submodule, not the lowest containing repository
Use the path of the containing repository of the current path, not the one the script is downloaded into
NathanJPhillips
force-pushed
the
bugfix/lint-work-across-repos
branch
from
2175b3d to
36dee83
Compare
|
Turns out I was an idiot with one of my previous changes here. I've undone that and made it all good now. |
scripts/filter_lint_by_diff.py
Outdated
There was a problem hiding this comment.
What was the purpose of # before? Are you sure you can remove that check?
6 participants
This PR makes the linter play nicely with our new sub-module layout.