Merge branch 'master' into develop

.gitlab-ci.yml

+workflow:
+  rules:
+    - if: $CI_PIPELINE_SOURCE == 'web'
+    - if: $CI_PIPELINE_SOURCE == 'merge_request_event'
+    - if: $CI_PIPELINE_SOURCE == 'parent_pipeline'
+    - if: $CI_COMMIT_TAG
+    - if: $CI_COMMIT_BRANCH == $CI_DEFAULT_BRANCH
+
 include:
+  # Runs on dev-profile/main in default branch, when merging to the default
+  # branch, and in "tag pipelines".
+  - project: bob/dev-profile
+    ref: main
+    file: gitlab/python.yml
+    rules:
+      - if: $CI_COMMIT_BRANCH == $CI_DEFAULT_BRANCH
+      - if: $CI_COMMIT_TAG
+      - if: $CI_MERGE_REQUEST_TARGET_BRANCH_NAME == $CI_DEFAULT_BRANCH
+  # Runs on dev-profile/develop in other branches (only when manually triggered)
+  # This is useful when trying new dependency pins in dev-profile/develop.
   - project: bob/dev-profile
     ref: develop
     file: gitlab/python.yml
+    rules:
+      - if: $CI_COMMIT_BRANCH == $CI_DEFAULT_BRANCH
+        when: never
+      - if: $CI_COMMIT_TAG
+        when: never
+      - if: $CI_MERGE_REQUEST_TARGET_BRANCH_NAME == $CI_DEFAULT_BRANCH
+        when: never
+      - when: always