Skip to content

Commit

Permalink
fix(scripts/deploy_nightly)
Browse files Browse the repository at this point in the history
  • Loading branch information
bryangingechen committed Mar 29, 2019
1 parent a4fd55c commit 9ca0104
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion scripts/deploy_nightly.sh
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ fi

# Try to update the lean-x.y.z branch on mathlib. This could fail if
# a subsequent commit has already pushed an update.
git push mathlib HEAD:$LEAN_VERSION || \
git push mathlib HEAD:refs/heads/$LEAN_VERSION || \
echo "mathlib rejected push to branch $LEAN_VERSION; maybe it already has a later version?" >&2

# Push the commits to a branch on nightly and push a tag.
Expand Down

0 comments on commit 9ca0104

Please sign in to comment.