Skip to content

Add repository property for tools input - #4037

Merged
mbg merged 12 commits into
mainfrom
mbg/repo-props/tools
Jul 24, 2026
Merged

Add repository property for tools input#4037
mbg merged 12 commits into
mainfrom
mbg/repo-props/tools

Conversation

@mbg

@mbg mbg commented Jul 22, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

This PR attempts to simplify and tidy up #3766 while resolving conflicts with recent changes to the codebase.

Compared with #3766, there are the following changes:

  • The repository property's behaviour is gated by a new FF.
  • There is no github-codeql-tools-mode property. The justification for this is that in Advanced Setup workflows, the tools input provided in the workflow takes precedence. The value of the repository property can be enforced with a prefix !. This is similar to the + notation for the queries input, where + means "combine rather than replace".
  • This PR does not change the telemetry to include the source of the effective tools value. However, it does lay the groundwork for it with the EffectiveInput type and getToolsInput returns a suitable value. Once we have merged relevant backend changes, the intention is to then make use of EffectiveInput values in the status reports. This will avoid duplication of work across similar inputs (i.e. rather than adding several new status reports properties for each, we will have an array of EffectiveInput values). That's outside the scope of this PR though.
  • Like