From bda961fc5b02b3b3f385855b911ee61c67a35814 Mon Sep 17 00:00:00 2001
From: Jephte Clain <Jephte.Clain@univ-reunion.fr>
Date: Sat, 13 Jan 2018 19:03:37 +0400
Subject: [PATCH] update-nutools: support de l'option --devel

---
 update-nutools | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/update-nutools b/update-nutools
index 1df08a2..dd2254b 100755
--- a/update-nutools
+++ b/update-nutools
@@ -51,7 +51,7 @@ NOTE: si une erreur se produit, utiliser l'adresse privée, e.g.
 fi
 
 case "$1" in
--d|--d|--dev|--develop) develop=develop;;
+-d|--d|--dev|--devel|--develop) develop=develop;;
 *) develop=;;
 esac