From 90ea6c6bd1ba319f7251a7e2eec525df0353fb32 Mon Sep 17 00:00:00 2001
From: Bob Lantz <rlantz@cs.stanford.edu>
Date: Mon, 23 Mar 2015 17:42:51 -0700
Subject: [PATCH] Usually kernel install is unnecessary, so don't quit if it
 fails

---
 util/install.sh | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/util/install.sh b/util/install.sh
index 25ab93d..2412f45 100755
--- a/util/install.sh
+++ b/util/install.sh
@@ -102,7 +102,10 @@ OF13_SWITCH_REV=${OF13_SWITCH_REV:-""}
 function kernel {
     echo "Install Mininet-compatible kernel if necessary"
     sudo apt-get update
-    $install linux-image-$KERNEL_NAME
+    if ! $install linux-image-$KERNEL_NAME; then
+        echo "Could not install linux-image-$KERNEL_NAME"
+        echo "Skipping - assuming installed kernel is OK."
+    fi
 }
 
 function kernel_clean {