Skip to content

chore: add a how-to guide on using devcontainers and codespaces#3947

Closed
signorecello wants to merge 4 commits intomasterfrom
zpedro/devcontainer_docs
Closed

chore: add a how-to guide on using devcontainers and codespaces#3947
signorecello wants to merge 4 commits intomasterfrom
zpedro/devcontainer_docs

Conversation

@signorecello
Copy link
Contributor

@signorecello signorecello commented Jan 4, 2024

Description

This PR adds a how-to guide on devcontainers and codespaces

Problem*

Resolves #3622

Summary*

  • Made a quick how-to guide on adding a devcontainer to a repository, so it can be used for codespaces
  • Quick explanation on what are devcontainers all about, since they wouldn't fit anywhere else without smashing context
  • Spent WAY MORE time than I should making a video and embedding it on the page

@github-actions github-actions bot added the documentation Improvements or additions to documentation label Jan 4, 2024
@signorecello signorecello requested review from a team and Savio-Sou January 4, 2024 12:51
@TomAFrench TomAFrench changed the title feat: adding a how-to guide on using devcontainers and codespaces chore: add a how-to guide on using devcontainers and codespaces Jan 4, 2024
@github-actions
Copy link
Contributor

github-actions bot commented Jan 4, 2024

Copy link
Contributor

@critesjosh critesjosh left a comment

Choose a reason for hiding this comment

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

Left a few small suggestions

@Savio-Sou
Copy link
Collaborator

Minor suggestions. Feel free to adopt / modify / dismiss as you see fit 🙏

@Savio-Sou
Copy link
Collaborator

Savio-Sou commented Jan 8, 2024

Separately noticed that the tone of this guide is on the more casual side.

While the lightheartedness is nice, do want to flag it in case @noir-lang/developerrelations would like to discuss tone consistency.

Copy link
Collaborator

@Savio-Sou Savio-Sou left a comment

Choose a reason for hiding this comment

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

Would be nice if the suggestions above could be reviewed first, but they don't necessarily have to block merging of this PR if needed.

@signorecello
Copy link
Contributor Author

merging this mf 😈 we should think about serving the videos somewhere else though, I'll think about it and revisit later

@signorecello signorecello enabled auto-merge January 9, 2024 12:30
@TomAFrench TomAFrench closed this Jan 10, 2024
auto-merge was automatically disabled January 10, 2024 09:52

Pull request was closed

@TomAFrench TomAFrench reopened this Jan 10, 2024
Copy link
Collaborator

@Savio-Sou Savio-Sou left a comment

Choose a reason for hiding this comment

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

Not sure if this is what was blocking the merge, but I'm seeing some "Pending" suggestions from my end.

image

(Re-)submitting a review comment to see if it helps.

UPDATE: Hmm they're still showing up with the "Pending" tag.

@signorecello
Copy link
Contributor Author

Yeah I'll just stop being a lazy bastard and will open another PR on the same branch

github-merge-queue bot pushed a commit that referenced this pull request Jan 11, 2024
# Description

Replaces #3947

---------

Co-authored-by: José Pedro Sousa <github@zepedro.me>
Co-authored-by: Cat McGee <helloworld@mcgee.cat>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

documentation Improvements or additions to documentation

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Document how Noir projects could better support GitHub Codespace using devcontainer.json

4 participants