From 3fab9a8970550f09c46818efb903dbe5e9e4bb0b Mon Sep 17 00:00:00 2001
From: mcarton <cartonmartin+git@gmail.com>
Date: Tue, 19 Jul 2016 21:57:40 +0200
Subject: [PATCH] Fix deploy.sh and python2 usage

---
 .github/deploy.sh | 2 +-
 util/export.py    | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

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 @@ 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"):