Skip to content
New issue

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

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

Already on GitHub? # to your account

remove stale/broken docker scripts, see #684 #1635

Merged
merged 1 commit into from
Sep 6, 2023
Merged

Conversation

alistairewj
Copy link
Member

Long discussion in #684

Summary is that the scripts are broken, and rather than have broken scripts, we should remove the build

Copy link
Member

@tompollard tompollard left a comment

Choose a reason for hiding this comment

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

Looks good to me, thanks! Closes #684

@tompollard tompollard merged commit 9169c23 into main Sep 6, 2023
5 checks passed
@tompollard tompollard deleted the remove_docker branch September 6, 2023 16:23
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants