shortcuts for public
Signed-off-by: Nico Schottelius <nico@kr.ethz.ch>
This commit is contained in:
parent
f44bc29789
commit
df9bdef75e
1 changed files with 1 additions and 1 deletions
2
build.sh
2
build.sh
|
@ -108,7 +108,7 @@ case "$1" in
|
||||||
cd ${WEBDIR} && make pub
|
cd ${WEBDIR} && make pub
|
||||||
;;
|
;;
|
||||||
|
|
||||||
pub)
|
p|pu|pub)
|
||||||
git push --mirror
|
git push --mirror
|
||||||
git push --mirror github
|
git push --mirror github
|
||||||
;;
|
;;
|
||||||
|
|
Loading…
Reference in a new issue