summaryrefslogtreecommitdiff
path: root/util/lint/lint
AgeCommit message (Expand)Author
2015-11-19lint: properly terminate junit report on errorPatrick Georgi
2015-10-31tree: drop last paragraph of GPL copyright headerPatrick Georgi
2015-10-17lint: Fix shellcheck warnings, add commentsMartin Roth
2015-10-17lint: Add junit.xml output for jenkinsMartin Roth
2015-10-17lint: Move the lint script out of Makefile.incMartin Roth