Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update the pico extras helper to fix fetching from git #713

Merged
merged 1 commit into from
Oct 7, 2021

Conversation

ali1234
Copy link
Contributor

@ali1234 ali1234 commented Sep 12, 2021

This fixes raspberrypi/pico-extras#24 so
that PICO_EXTRAS_FETCH_FROM_GIT works.

This fixes raspberrypi/pico-extras#24 so
that PICO_EXTRAS_FETCH_FROM_GIT works.
@ali1234
Copy link
Contributor Author

ali1234 commented Sep 12, 2021

Note that a pull request against the pico extras repo is pending.

@Gadgetoid Gadgetoid merged commit a8b4e3d into 32blit:master Oct 7, 2021
@Gadgetoid
Copy link
Contributor

Thank you! Should make this a touch easier for beginners!

@ali1234 ali1234 deleted the pico-extras-fix branch October 22, 2021 22:04
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.

PICO_EXTRAS_FETCH_FROM_GIT does not work
2 participants