diff options
Diffstat (limited to 'devscripts/release.sh')
| -rwxr-xr-x | devscripts/release.sh | 4 | 
1 files changed, 0 insertions, 4 deletions
| diff --git a/devscripts/release.sh b/devscripts/release.sh index 796468b4b..2766174c1 100755 --- a/devscripts/release.sh +++ b/devscripts/release.sh @@ -88,10 +88,6 @@ ROOT=$(pwd)      "$ROOT/devscripts/gh-pages/update-sites.py"      git add *.html *.html.in update      git commit -m "release $version" -    git show HEAD -    read -p "Is it good, can I push? (y/n) " -n 1 -    if [[ ! $REPLY =~ ^[Yy]$ ]]; then exit 1; fi -    echo      git push "$ROOT" gh-pages      git push "$ORIGIN_URL" gh-pages  ) | 
