From 6ddb870a56560c92e9a5dfeed602027b1912201a Mon Sep 17 00:00:00 2001
From: Jephte Clain <Jephte.Clain@univ-reunion.fr>
Date: Mon, 7 Aug 2023 13:40:31 +0400
Subject: [PATCH] dkbuild: support profil nu

---
 dkbuild | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/dkbuild b/dkbuild
index eb7b75e..21f91a5 100755
--- a/dkbuild
+++ b/dkbuild
@@ -1418,6 +1418,14 @@ function resolve_dists_profiles() {
     }
     load_dkbuild
 
+    if [ -z "$SETPROFILES_DONE" -a -n "$PROFILE" ]; then
+        # Si l'utilisateur spécifie un profil mais qu'aucun profil n'a été
+        # défini dans la configuration, considérer que c'est cet unique profil
+        # qui a été défini
+        SETPROFILES=("$PROFILE")
+        SETPROFILES_DONE=1
+    fi
+
     ## ensuite vérifier si on est dans la bonne distribution
     edebug "Calcul de la distribution courante"
     reset_functions