Only push the tag that we are interested in for the release.

mockingbirdnest · Mar 19, 2023 · 099e122 · 099e122
1 parent dd49404
commit 099e122
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/make_principia_release.ps1 b/make_principia_release.ps1
@@ -118,5 +118,5 @@ if ($mathematician.contains("TEST")) {
   echo "  git tag --delete $tag"
   echo "to clean up."
 } else {
-  git push $remote --tags
+  git push $remote $tag
 }