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

Wget and curl both do the same thing. Remove wget and use only curl. #434

Merged
merged 1 commit into from
Mar 18, 2024

Conversation

arjo129
Copy link
Contributor

@arjo129 arjo129 commented Mar 18, 2024

I noticed that we ask users to install both wget and curl when installing from source. This feels redundant.

I noticed that we ask users to install both `wget` and `curl`. This feels redundant.

Signed-off-by: Arjo Chakravarty <[email protected]>
@github-actions github-actions bot added the 🎵 harmonic Gazebo Harmonic label Mar 18, 2024
@ahcorde ahcorde merged commit a6717da into master Mar 18, 2024
2 checks passed
@ahcorde ahcorde deleted the docs/remove_wget branch March 18, 2024 07:59
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
🎵 harmonic Gazebo Harmonic
Projects
Archived in project
Development

Successfully merging this pull request may close these issues.

2 participants