add support for gentoo to explorer os

Signed-off-by: Steven Armstrong <steven.armstrong@inf.ethz.ch>
12 years ago · f3584aa727
1 changed files with 2 additions and 0 deletions
--- 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