bootstrap: rename 'user' profile to 'dist'

1 files changed, 8 insertions, 0 deletions

diff --git a/src/bootstrap/config.rs b/src/bootstrap/config.rs
index 8ee63e561ba..b91275e73e9 100644
--- a/src/bootstrap/config.rs
+++ b/src/bootstrap/config.rs
@@ -1129,6 +1129,14 @@ impl Config {
         };
 
         if let Some(include) = &toml.profile {
+            // Allows creating alias for profile names, allowing
+            // profiles to be renamed while maintaining back compatibility
+            // Keep in sync with `profile_aliases` in bootstrap.py
+            let profile_aliases = HashMap::from([("user", "dist")]);
+            let include = match profile_aliases.get(include.as_str()) {
+                Some(alias) => alias,
+                None => include.as_str(),
+            };
             let mut include_path = config.src.clone();
             include_path.push("src");
             include_path.push("bootstrap");