master: fix -delete -> --delete.

coin-or · May 31, 2024 · 083a11c · 083a11c
1 parent 69e2b71
commit 083a11c
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/bin/new_release.sh b/bin/new_release.sh
@@ -47,7 +47,7 @@ then
    echo "The tag $tag already exists"
    echo 'Use the follow commands to delete it ?'
    echo "   git tag -d $tag"
-   echo "   git push -delete origin $tag"
+   echo "   git push --delete origin $tag"
    exit 1
 fi
 #