From e488482a2cbac9d72821b9d07f063c9abff40069 Mon Sep 17 00:00:00 2001
From: Giovanni Campagna <gcampagna@src.gnome.org>
Date: Mon, 28 Nov 2011 16:15:36 +0100
Subject: [PATCH] Introduce local-install.sh script

Cherry-picked from master.
---
 local-install.sh | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100755 local-install.sh

diff --git a/local-install.sh b/local-install.sh
new file mode 100755
index 00000000..2a3ef0df
--- /dev/null
+++ b/local-install.sh
@@ -0,0 +1,15 @@
+#!/bin/bash
+
+extensionbase=~/.local/share/gnome-shell/extensions
+
+for i in zip-files/*; do
+    zip_file=`pwd`/$i;
+    uuid=`basename $i | sed -e "s/.shell-extension.zip//"`;
+    if [ -d $extensionbase/$uuid ]; then
+	rm -fR $extensionbase/$uuid;
+    fi
+    mkdir $extensionbase/$uuid;
+    (cd $extensionbase/$uuid;
+	unzip -q $zip_file;
+    );
+done