From 2e200535fb7b7cbf842999c8f674e737f40ef773 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 26 Jul 2017 17:17:48 +0200 Subject: [PATCH] chore(script/deploy_gh_pages): upload to new lean-nightly repo --- script/deploy_gh_pages.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/script/deploy_gh_pages.sh b/script/deploy_gh_pages.sh index e7dceb740f..7da8fec7c0 100644 --- a/script/deploy_gh_pages.sh +++ b/script/deploy_gh_pages.sh @@ -6,7 +6,7 @@ set -eu rev=$(git rev-parse --short HEAD) -git clone -b gh-pages "https://$GH_TOKEN@github.com/$TRAVIS_REPO_SLUG.git" gh-pages +git clone -b gh-pages "https://$GH_TOKEN@github.com/leanprover/lean-nightly.git" gh-pages cd gh-pages mkdir -p build