use same name for github everywhere

Signed-off-by: Jeff Carr <jcarr@wit.com>
2024-01-05 20:14:38 -06:00 · 2024-01-05 20:14:38 -06:00 · cfd827bbdd
parent 8d7fc91f65
commit cfd827bbdd
1 changed files with 4 additions and 2 deletions
--- a/6
+++ b/6
@ -25,6 +25,8 @@ update:
 # git branch -M master
 github:
 	git push origin master
+	git push origin devel
 	git push origin --tags
-	git push github2 master
-	git push github2 --tags
+	git push github master
+	git push github devel
+	git push github --tags