From d211d532645f566b0f79a0403b6b6be61aa05b22 Mon Sep 17 00:00:00 2001 From: Kevin Veen-Birkenbach Date: Tue, 20 Jun 2023 20:38:09 +0200 Subject: [PATCH] Solved bug --- gnome-extension-manager.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/gnome-extension-manager.sh b/gnome-extension-manager.sh index b2a1d4c..480f682 100644 --- a/gnome-extension-manager.sh +++ b/gnome-extension-manager.sh @@ -15,6 +15,7 @@ echo "Installing GNOME extension \"$extension_name\"..." if [ "$action_type" == "enable" ]; then if [ ! -z "$extension_repository_path" ]; then + echo "Generating extension based on $3" if [ -d "$extension_folder" ]; then if [ -d "$extension_folder.git" ]; then echo "Pulling changes from git..."