diff --git a/.github/deploy.sh b/.github/deploy.sh index 7b40371e01b1..15b14e64a78d 100755 --- a/.github/deploy.sh +++ b/.github/deploy.sh @@ -24,7 +24,7 @@ rm -rf out/master/ || exit 0 # Make the doc for master mkdir out/master/ cp util/gh-pages/index.html out/master -./util/export.py out/master/lints.json +python ./util/export.py out/master/lints.json # Save the doc for the current tag and point current/ to it if [ -n "$TRAVIS_TAG" ]; then diff --git a/util/export.py b/util/export.py index 558209eee4d3..8d95c70f1e77 100755 --- a/util/export.py +++ b/util/export.py @@ -21,15 +21,15 @@ # TODO: actual logging def warn(*args): - print(*args) + print(args) def debug(*args): - print(*args) + print(args) def info(*args): - print(*args) + print(args) def parse_path(p="clippy_lints/src"):