Skip to content

Rename commands page to "instrumentation"#3663

Merged
josephsnyder merged 1 commit intoKitware:masterfrom
williamjallen:rename-commands-page
Apr 17, 2026
Merged

Rename commands page to "instrumentation"#3663
josephsnyder merged 1 commit intoKitware:masterfrom
williamjallen:rename-commands-page

Conversation

@williamjallen
Copy link
Copy Markdown
Collaborator

The distinction between the build commands page (which exclusively displays instrumentation data) and the build targets page (which is currently only useful if instrumentation data was submitted, but is intended to be used without instrumentation in the future) is currently unclear to users. This PR renames the build commands page to build "instrumentation".

The distinction between the build commands page (which exclusively displays instrumentation data) and the build targets page (which is currently only useful if instrumentation data was submitted, but is intended to be used without instrumentation in the future) is currently unclear to users.  This PR renames the build commands page to build "instrumentation".
Copy link
Copy Markdown
Member

@josephsnyder josephsnyder left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM!

@josephsnyder josephsnyder added this pull request to the merge queue Apr 17, 2026
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Apr 17, 2026
@josephsnyder josephsnyder added this pull request to the merge queue Apr 17, 2026
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Apr 17, 2026
@josephsnyder josephsnyder added this pull request to the merge queue Apr 17, 2026
Merged via the queue into Kitware:master with commit 39656cc Apr 17, 2026
7 checks passed
@williamjallen williamjallen deleted the rename-commands-page branch April 17, 2026 16:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants