updated makefile

main
Philipp3107 2022-12-20 12:58:52 +01:00
parent 63f45cb9c0
commit de13ede97d
1 changed files with 8 additions and 1 deletions

View File

@ -15,6 +15,13 @@ update_domain:
git add domain/ git add domain/
git commit -m "Updated domain. Further explanation in README" git commit -m "Updated domain. Further explanation in README"
git push -u origin main git push -u origin main
update_exceptions:
git add robot/exceptions
git commit -m "Updated Exceptions"
git push -u origin main
update_interfaces:
git add robot/interfaces
git commit -m "updated interfaces"
git push -u origin main
fetch_git: fetch_git:
git pull origin main git pull origin main