diff options
Diffstat (limited to '.github')
| -rwxr-xr-x | .github/deploy.sh | 2 |
1 files changed, 1 insertions, 1 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 |