Repository navigation

docs_update: Skip if a PR is already open - #2242

Merged

Urgau merged 2 commits into

rust-lang:masterfrom

ehuss:docs-update-skip-open-pr

Jan 1, 2026

Merged

docs_update: Skip if a PR is already open#2242
Urgau merged 2 commits into
rust-lang:masterfrom
ehuss:docs-update-skip-open-pr

Commits on Dec 31, 2025
- docs_update: Skip if a PR is already open
  ehuss
  committed
  7d275ff
Commits on Jan 1, 2026
- Add context to is_pr_already_open error
  ehuss
  committed
  64b38dd