From df9bdef75e1554a87f3639d832e572bec4e7a21f Mon Sep 17 00:00:00 2001
From: Nico Schottelius <nico@kr.ethz.ch>
Date: Tue, 26 Jul 2011 21:56:19 +0200
Subject: [PATCH] shortcuts for public

Signed-off-by: Nico Schottelius <nico@kr.ethz.ch>
---
 build.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/build.sh b/build.sh
index eded032e..a6897d49 100755
--- a/build.sh
+++ b/build.sh
@@ -108,7 +108,7 @@ case "$1" in
       cd ${WEBDIR} && make pub
    ;;
 
-   pub)
+   p|pu|pub)
       git push --mirror
       git push --mirror github
    ;;