diff options
| author | mcarton <cartonmartin+git@gmail.com> | 2016-07-19 21:57:40 +0200 |
|---|---|---|
| committer | mcarton <cartonmartin+git@gmail.com> | 2016-07-19 22:07:39 +0200 |
| commit | 3fab9a8970550f09c46818efb903dbe5e9e4bb0b (patch) | |
| tree | 15a45a623de2f5475293bdd734da25361bf29e83 | |
| parent | b7df2f8732679683f306b751b7f60aff1d98e3a9 (diff) | |
Fix deploy.sh and python2 usage
| -rwxr-xr-x | .github/deploy.sh | 2 | ||||
| -rwxr-xr-x | util/export.py | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/.github/deploy.sh b/.github/deploy.sh index 7b40371e01b..15b14e64a78 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 558209eee4d..8d95c70f1e7 100755 --- a/util/export.py +++ b/util/export.py @@ -21,15 +21,15 @@ This lint has the following configuration variables: # 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"): |