From 41e07102c757b3e1d59bb9233fa90886364675db Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nicolas=20Hord=C3=A9?= <nicolas@palon.fr>
Date: Sat, 19 Sep 2020 20:31:41 +0200
Subject: [PATCH] build: fix du commentaire dans menu.sh

---
 menu.sh | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/menu.sh b/menu.sh
index 88a65a3..42f25b7 100755
--- a/menu.sh
+++ b/menu.sh
@@ -83,9 +83,9 @@ else
 fi
 if [ "${CHOOSE}" != "" ]; then
 	echo "*** Application de la version ${CHOOSE}"
-	#dgit checkout $CHOOSE
-	#dgit clean -fd
-	#dgit reset --hard
+	git checkout $CHOOSE
+	git clean -fd
+	git reset --hard
 	./make.sh tool
 fi
 read