From 84f11659f1fb54091d3c17d6763516ea453cc09d Mon Sep 17 00:00:00 2001 From: Simon Schneegans Date: Wed, 22 Feb 2023 10:50:38 +0100 Subject: [PATCH] :wrench: Give application profiles a higher priority --- src/ProfileManager.js | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/ProfileManager.js b/src/ProfileManager.js index fcad182..4de9aba 100644 --- a/src/ProfileManager.js +++ b/src/ProfileManager.js @@ -133,8 +133,12 @@ var ProfileManager = class { getProfilePriority(settings) { let priority = 0; - // Each setting which is not set to its default value increases the priority by one. - if (settings.get_string('profile-app') != '') ++priority; + // If an application is specified, we increase the priority quite a lot. This makes + // sure that per-application overrides are used in most cases. + if (settings.get_string('profile-app') != '') priority += 10; + + // Each other setting which is not set to its default value increases the priority by + // one. if (settings.get_int('profile-animation-type') > 0) ++priority; if (settings.get_int('profile-window-type') > 0) ++priority; if (settings.get_int('profile-color-scheme') > 0) ++priority;