From e55e18e4ce95cd924997fa0c5d34c53793b45085 Mon Sep 17 00:00:00 2001
From: Bob Lantz <rlantz@cs.stanford.edu>
Date: Tue, 9 May 2017 14:09:42 -0700
Subject: [PATCH] Treat Raspbian as Debian; add $DISTS.

Fixes #713
---
 util/install.sh | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/util/install.sh b/util/install.sh
index fc724f0..9961681 100755
--- a/util/install.sh
+++ b/util/install.sh
@@ -80,8 +80,12 @@ echo "Detected Linux distribution: $DIST $RELEASE $CODENAME $ARCH"
 KERNEL_NAME=`uname -r`
 KERNEL_HEADERS=kernel-headers-${KERNEL_NAME}
 
-if ! echo $DIST | egrep 'Ubuntu|Debian|Fedora|RedHatEnterpriseServer|SUSE LINUX'; then
-    echo "Install.sh currently only supports Ubuntu, Debian, RedHat and Fedora."
+# Treat Raspbian as Debian
+[ "$DIST" = 'Raspbian' ] && DIST='Debian'
+
+DISTS='Ubuntu|Debian|Fedora|RedHatEnterpriseServer|SUSE LINUX'
+if ! echo $DIST | egrep "$DISTS" >/dev/null; then
+    echo "Install.sh currently only supports $DISTS."
     exit 1
 fi