Skip to content

main: fix picotool info for non-partition-capable devices#338

Merged
will-v-pi merged 1 commit into
raspberrypi:developfrom
intelfx:work/fix-picotool-info
Jul 14, 2026
Merged

main: fix picotool info for non-partition-capable devices#338
will-v-pi merged 1 commit into
raspberrypi:developfrom
intelfx:work/fix-picotool-info

Conversation

@intelfx

@intelfx intelfx commented Jul 10, 2026

Copy link
Copy Markdown
Contributor

Fixes #336.

@intelfx

intelfx commented Jul 10, 2026

Copy link
Copy Markdown
Contributor Author

To maintainers, please change the default PR target in repo settings from master to develop — I used GH CLI to submit a PR against the default target branch only to have a bot tell me that the target branch is wrong.

@lurch

lurch commented Jul 11, 2026

Copy link
Copy Markdown
Contributor

To maintainers, please change the default PR target in repo settings from master to develop — I used GH CLI to submit a PR against the default target branch only to have a bot tell me that the target branch is wrong.

AFAIK, GitHub doesn't have a "default PR target" setting, it only has a "default branch" setting - and we have the default branch set to master, because that's the branch we want most people to use when cloning and building this repo. (Hence why we added the separate CI check that PRs are targetting the correct branch 😉 )

Note that you didn't have to close your earlier #337 PR and open this new one - you could have just clicked on the pencil icon next to the PR title and change the PR's base-branch directly. (IMHO it's a bit confusing that GitHub have decided to hide that option inside the "Edit title" button!)

@will-v-pi will-v-pi left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Thanks for this fix

@will-v-pi
will-v-pi merged commit d469aeb into raspberrypi:develop Jul 14, 2026
42 checks passed
@will-v-pi

Copy link
Copy Markdown
Contributor

This fix has been cherry-picked into master

@intelfx

intelfx commented Jul 15, 2026

Copy link
Copy Markdown
Contributor Author

@lurch Right, yeah, sorry. For some reason I was entirely sure there were distinct default branches for the repo and the PRs.

There was no option to retarget the PR, though (I checked).

@lurch

lurch commented Jul 15, 2026

Copy link
Copy Markdown
Contributor

There was no option to retarget the PR, though (I checked).

There is, it's just hidden inside the "Edit title" option. (But obviously you can't change the base branch on already-merged PRs 😉 )
image

@intelfx

intelfx commented Jul 15, 2026

Copy link
Copy Markdown
Contributor Author

I mean, I know about this feature, but it isn't offered on my PR (and wasn't, while it was open):
image

@lurch

lurch commented Jul 15, 2026

Copy link
Copy Markdown
Contributor

Fair enough, perhaps GitHub have changed things so that only repo-admins get that option now? 🤷

@lurch

lurch commented Jul 16, 2026

Copy link
Copy Markdown
Contributor

Fair enough, perhaps GitHub have changed things so that only repo-admins get that option now? 🤷

No need to panic, looks like PR-authors can change the base-branch on their still-open PRs 🙂 #346

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants