From f3584aa727ecb6c395c204ef1204695a143c5457 Mon Sep 17 00:00:00 2001
From: Steven Armstrong <steven.armstrong@inf.ethz.ch>
Date: Tue, 8 Feb 2011 11:01:47 +0100
Subject: [PATCH] add support for gentoo to explorer os

Signed-off-by: Steven Armstrong <steven.armstrong@inf.ethz.ch>
---
 conf/explorers/os | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/conf/explorers/os b/conf/explorers/os
index 3bd3f2ef..41d70545 100755
--- a/conf/explorers/os
+++ b/conf/explorers/os
@@ -32,6 +32,8 @@ fi
 
 [ -f /etc/debian_version ] && echo debian
 
+[ -f /etc/gentoo-release ] && echo gentoo
+
 [ -f /etc/redhat-release ] && echo redhat
 
 # ensure correct exit, otherwise other explorer won't get started