Fix docs path exclusion to use recursive wildcard in azure-pipelines-PR.yml

[Copilot]

docs/* only excludes direct children of docs/, so changes to nested paths like docs/release-notes/foo.md were still triggering CI builds.

Change

Replace docs/* with docs/** in both trigger.paths.exclude and pr.paths.exclude:

exclude:
  - docs/**   # was: docs/*

** matches at any nesting depth, so all changes under docs/ are now correctly excluded from both push and PR triggers.

Original prompt

Update azure-pipelines-PR.yml in dotnet/fsharp so changes anywhere under /docs/, at any nesting depth, are excluded from triggering CI.

Current file uses docs/* in path exclusions, which can miss nested paths like docs/release-notes/.... Change the docs path exclusion under both the trigger.paths.exclude and pr.paths.exclude sections to use a recursive wildcard such as docs/**.

Scope:

• Modify only the Azure Pipelines path filters needed for this behavior.
• Ensure both CI triggers and PR triggers exclude all nested paths under docs/.
• Preserve existing formatting and unrelated exclusions.

Acceptance criteria:

• trigger.paths.exclude contains docs/** instead of docs/*.
• pr.paths.exclude contains docs/** instead of docs/*.
• No unrelated pipeline behavior is changed.

The following is the prior conversation context from the user's chat exploration (may be truncated):

User: Why are file changes inside docs/release-notes or so still causing a CI re-run ? Do we need different wildcard for nested subpaths?

Assistant: Yes — use a recursive path pattern. In this file, docs/* is likely only excluding direct children of docs, not nested files like docs/release-notes/foo.md. For nested subpaths, use docs/** or, if you only want that area, docs/release-notes/**.

Update both trigger.paths.exclude and pr.paths.exclude:

trigger:
  paths:
    include:
    - '*'
    exclude:
    - .github/**
    - docs/**
    - .vscode/**
    - .devcontainer/**
    - tests/scripts/**
    - attributions.md
    - CODE_OF_CONDUCT.md
    - DEVGUIDE.md
    - INTERNAL.md
    - Language-Version-History.md
    - License.txt
    - README.md
    - release-notes.md
    - TESTGUIDE.md

pr:
  paths:
    include:
    - '*'
    exclude:
    - .github/**
    - docs/**
    - .vscode/**
    - .devcontainer/**
    - tests/scripts/**
    - attributions.md
    - CODE_OF_CONDUCT.md
    - DEVGUIDE.md
    - INTERNAL.md
    - Language-Version-History.md
    - License.txt
    - README.md
    - release-notes.md
    - TESTGUIDE.md

Azure Pipelines supports **, *, and ? in path filters, and Microsoft’s docs specifically show ** for recursive matching like src/app/**/myapp*. Paths are repo-root-relative, case-sensitive, and include filters are processed before excludes; order does not matter. (learn.microsoft.com)

A few gotchas:

• release-notes.md only excludes the root file release-notes.md; it does not exclude docs/release-notes/....
• If a PR changes both docs/release-notes/... and some non-excluded file, CI will still run.
• For GitHub PR validation, Azure evaluates the YAML from the PR merge result, so a PR changing the YAML can affect its own trigger behavior. (learn.microsoft.com)
• If Azure is correctly skipping due to path filters, GitHub may still receive a neutral status rather than a full build. (learn.microsoft.com)

User: Can you raise a PR changing that? Anything under /docs/, no matter how deep, should be excluded from triggering CI run

Assistant: I’m waiting for your confirmation to proceed with creating the PR.

This pull request was created from Copilot chat.

[T-Gro]

LGTM — the change is correct and well-scoped.

One optional follow-up: the same single-star limitation applies to .github/, .vscode/, .devcontainer/, and ests/scripts/ in both sections. If any of those directories have nested content (e.g. .github/workflows/*.yml), they'd also benefit from **. Feel free to address in a separate PR or ignore if those dirs are flat today.

[github-actions]

✅ No release notes required