make git push

2023-10-31 10:14:58 -06:00 · 2023-10-31 10:14:58 -06:00 · 0768591e91
parent f9badc43a3
commit 0768591e91
2 changed files with 12 additions and 0 deletions
--- a/BUILD.md
+++ b/BUILD.md
@ -60,3 +60,11 @@ Clean.
 ```
 make clean
 ```
+
+
+# Push
+Push to git repo.
+
+```
+make push
+```
--- a/4
+++ b/4
@ -26,3 +26,7 @@ aiserver:

 clean:
 	$(MAKE) clean -C src
+
+push:
+	git push
+	git push --tags