[PATCH] changed the used shell and respective calls to /bin/sh Signed-Off-By: J <offlineimap at 927589452.de>

[offlineimap at 927589452.de]

From: Jens Heinrich <admin at high5.alioth.uberspace.de>

---
 scripts/get-repository.sh | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/scripts/get-repository.sh b/scripts/get-repository.sh
index a6dad95..5e7df38 100755
--- a/scripts/get-repository.sh
+++ b/scripts/get-repository.sh
@@ -1,6 +1,6 @@
-#!/bin/bash
+#!/bin/sh
 #
-# Licence: this file is in the public deomain.
+# Licence: this file is in the public domain.
 #
 # Download and configure the repositories of the website or wiki.
 
@@ -10,7 +10,7 @@ github_remote=$2
 #
 # TODO
 #
-function final_note () {
+final_note () {
 	cat <<EOF
 
 Now, you can fork the repository into Github from $2
@@ -22,7 +22,7 @@ and add a reference to it in your local copy:
 EOF
 }
 
-function setup () {
+setup () {
 	target_dir=$1
 	remote_url=$2
 
@@ -49,7 +49,7 @@ function setup () {
 	fi
 }
 
-function configure_website () {
+configure_website () {
 	renderer='./render.sh'
 
 	echo "Found Github username: '$1'"
@@ -65,7 +65,7 @@ function configure_website () {
 	fi
 }
 
-function configure_wiki () {
+configure_wiki () {
 	:	# noop
 }
 
-- 
2.11.0