Setup automatic push of gh-pages

This commit is contained in:
mcarton 2016-07-19 21:25:46 +02:00
parent c638e5b679
commit 01c61a714b
No known key found for this signature in database
GPG key ID: 5E427C794CBA45E8
4 changed files with 92 additions and 5 deletions

66
.github/deploy.sh vendored Executable file
View file

@ -0,0 +1,66 @@
#!/bin/bash
# Automatically deploy on gh-pages
set -e
SOURCE_BRANCH="master"
TARGET_BRANCH="gh-pages"
# Save some useful information
REPO=$(git config remote.origin.url)
SSH_REPO=${REPO/https:\/\/github.com\//git@github.com:}
SHA=$(git rev-parse --verify HEAD)
# Clone the existing gh-pages for this repo into out/
(
git clone "$REPO" out
cd out
git checkout $TARGET_BRANCH
)
# Remove the current doc for master
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
# Save the doc for the current tag and point current/ to it
if [ -n "$TRAVIS_TAG" ]; then
cp -r out/master "out/$TRAVIS_TAG"
rm -f out/current
ln -s "$TRAVIS_TAG" out/current
fi
# Pull requests and commits to other branches shouldn't try to deploy, just build to verify
if [ "$TRAVIS_PULL_REQUEST" != "false" ] || [ "$TRAVIS_BRANCH" != "$SOURCE_BRANCH" ]; then
echo "Generated, won't push"
exit 0
fi
# Now let's go have some fun with the cloned repo
cd out
git config user.name "Travis CI"
git config user.email "travis@ci.invalid"
if [ -z "$(git diff --exit-code)" ]; then
echo "No changes to the output on this push; exiting."
exit 0
fi
git add .
git commit -m "Automatic deploy to GitHub Pages: ${SHA}"
# Get the deploy key by using Travis's stored variables to decrypt deploy_key.enc
ENCRYPTED_KEY_VAR="encrypted_${ENCRYPTION_LABEL}_key"
ENCRYPTED_IV_VAR="encrypted_${ENCRYPTION_LABEL}_iv"
ENCRYPTED_KEY=${!ENCRYPTED_KEY_VAR}
ENCRYPTED_IV=${!ENCRYPTED_IV_VAR}
openssl aes-256-cbc -K "$ENCRYPTED_KEY" -iv "$ENCRYPTED_IV" -in deploy_key.enc -out deploy_key -d
chmod 600 deploy_key
eval $(ssh-agent -s)
ssh-add deploy_key
# Now that we're all set up, we can push.
git push "$SSH_REPO" "$TARGET_BRANCH"

BIN
.github/deploy_key.enc vendored Normal file

Binary file not shown.

4
.gitignore vendored
View file

@ -1,3 +1,7 @@
# Used by Travis to be able to push:
/.github/deploy_key
out
# Compiled files
*.o
*.so

View file

@ -1,8 +1,11 @@
#!/usr/bin/env python
# Build the gh-pages
import json
import os
import re
import json
import sys
level_re = re.compile(r'''(Forbid|Deny|Warn|Allow)''')
conf_re = re.compile(r'''define_Conf! {\n([^}]*)\n}''', re.MULTILINE)
@ -15,10 +18,19 @@ This lint has the following configuration variables:
* `%s: %s`: %s (defaults to `%s`).
"""
# TODO: actual logging
def warn(*args): print(args)
def debug(*args): print(args)
def info(*args): print(args)
def warn(*args):
print(*args)
def debug(*args):
print(*args)
def info(*args):
print(*args)
def parse_path(p="clippy_lints/src"):
lints = []
@ -52,6 +64,7 @@ def parse_conf(p):
return c
def parseLintDef(level, comment, name):
lint = {}
lint['id'] = name
@ -80,6 +93,7 @@ def parseLintDef(level, comment, name):
return lint
def parse_file(d, f):
last_comment = []
comment = True
@ -134,10 +148,13 @@ def parse_file(d, f):
warn("Warning: Missing Lint-Name in", f)
comment = True
def main():
lints = parse_path()
info("got %s lints" % len(lints))
with open("util/gh-pages/lints.json", "w") as file:
outdir = sys.argv[1] if len(sys.argv) > 1 else "util/gh-pages/lints.json"
with open(outdir, "w") as file:
json.dump(lints, file, indent=2)
info("wrote JSON for great justice")