From c7b5042f921185615b471a2c01ce3db157b427f9 Mon Sep 17 00:00:00 2001
From: ianb <ianb>
Date: Thu, 16 Dec 2010 18:22:16 +0000
Subject: [PATCH] Explicitly mark perms.sh-dist as a bash script.

perms.sh-dist has bashisms, so would fail on a system (eg some recent
Debian systems) with dash as /bin/sh.
---
 perms.sh-dist | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/perms.sh-dist b/perms.sh-dist
index ae9f3129..0711ab35 100755
--- a/perms.sh-dist
+++ b/perms.sh-dist
@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/bin/bash
 
 # Where the installed system resides
 INSTDIR=`dirname $0`/bin/mir
-- 
2.11.0