From 7c7d693bd5b7df4c2f1471537241915f8e37a40e Mon Sep 17 00:00:00 2001
From: Jens Heinrich <admin@high5.alioth.uberspace.de>
Date: Mon, 30 Jan 2017 14:59:36 +0100
Subject: [PATCH] scripts/get-repository.sh: use portable /bin/sh

Signed-off-by: J <offlineimap@927589452.de>
Signed-off-by: Nicolas Sebrecht <nicolas.s-dev@laposte.net>
---
 scripts/get-repository.sh     | 10 +++++-----
 scripts/get-repository.sh.rej | 10 ++++++++++
 2 files changed, 15 insertions(+), 5 deletions(-)
 create mode 100644 scripts/get-repository.sh.rej

diff --git a/scripts/get-repository.sh b/scripts/get-repository.sh
index 4258e8f..5e7df38 100755
--- a/scripts/get-repository.sh
+++ b/scripts/get-repository.sh
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
 #
 # Licence: this file is in the public domain.
 #
@@ -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
 }
 
diff --git a/scripts/get-repository.sh.rej b/scripts/get-repository.sh.rej
new file mode 100644
index 0000000..e3cdb80
--- /dev/null
+++ b/scripts/get-repository.sh.rej
@@ -0,0 +1,10 @@
+diff a/scripts/get-repository.sh b/scripts/get-repository.sh	(rejected hunks)
+@@ -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.
+