From 75e761637c7a1ce487ce68ade8a8b7fa7fcea343 Mon Sep 17 00:00:00 2001
From: Eugenio Parodi <ceccopierangiolieugenio@googlemail.com>
Date: Fri, 27 Oct 2023 17:50:31 +0100
Subject: [PATCH] Makefile

---
 Makefile | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Makefile b/Makefile
index af924b44..f1294a48 100644
--- a/Makefile
+++ b/Makefile
@@ -84,9 +84,9 @@ deployDoc:
 	git checkout gh-pages
 
 	# Update the doc files
-	rm -rf *.inv *.html *.js _* autogen.* tutorial
+	rm -rf *.inv *.html *.js _* autogen.* tutorial info
 	cp -a docs/build/html/* .
-	find *.html *.inv *.js autogen.TermTk _* tutorial | xargs git add
+	find *.html *.inv *.js autogen.TermTk _* tutorial info | xargs git add
 
 	git commit -m "Doc Updated"
 	git push origin gh-pages