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