Also for stats report which repo and which job number use our setup

[neurodebian.git] / survey / select_os_options.inc

diff --git a/survey/select_os_options.inc b/survey/select_os_options.inc
index 18693d07baaef88ff014c5c8da038330fc1cbcd7..8b92394ea097252d2c288b29a91eb53df3723c62 100644 (file)
--- a/survey/select_os_options.inc
+++ b/survey/select_os_options.inc
@@ -7,6 +7,7 @@
 <option value="scilinux" label="Scientific Linux">Scientific Linux</option>
 <option value="debian" label="Debian">Debian</option>
 <option value="ubuntu" label="Ubuntu">Ubuntu</option>
+<option value="mint" label="Linux Mint">Linux Mint</option>
 <option value="biolinux" label="BioLinux">BioLinux</option>
 <option value="slel" label="Suse Enterprise Linux">Suse Enterprise Linux</option>
 <option value="suse" label="OpenSuse">OpenSuse</option>