also push to github by default
Signed-off-by: Nico Schottelius <nico@kr.ethz.ch>
This commit is contained in:
parent
a729e05132
commit
e392792e1e
1 changed files with 2 additions and 1 deletions
3
Makefile
3
Makefile
|
@ -174,7 +174,8 @@ t2:
|
|||
# Developer targets
|
||||
#
|
||||
pub:
|
||||
@git push
|
||||
git push
|
||||
git push github
|
||||
|
||||
publish-doc: documentation
|
||||
@echo "Transferring files to ${host}"
|
||||
|
|
Loading…
Reference in a new issue