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