1 files changed, 16 insertions, 0 deletions
diff --git a/git.liw.fi.sh b/git.liw.fi.sh
index 6f20266..d7df0b5 100644
--- a/git.liw.fi.sh
+++ b/git.liw.fi.sh
@@ -118,6 +118,22 @@ clone_with_ssh()
 }
 
 
+# Push repo over ssh.
+
+push_with_ssh()
+{
+    local user="$1"
+    shift
+    if [ "$user" = admin ]
+    then
+	git push "$@"
+    else
+	KEYFILE="$DATADIR/$user.key" \
+	    PATH="$SRCDIR:$PATH" git push "$@"
+    fi
+}
+
+
 # Remove a repository from the server. This is a two-step process.
 
 destroy_repo()