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

Improve interactive docker/bash.sh #6344

Closed
wants to merge 26 commits into from

Conversation

areusch
Copy link
Contributor

@areusch areusch commented Aug 26, 2020

Some fixes to hopefully improve docker/bash.sh for use in local development:

  • properly quote command-line arguments
  • mount repo at $(pwd) by default; fixes problems when using git-worktree.

Don't know how the latter change will impact the CI, but let's see if it breaks it too badly first.

@tqchen tqchen changed the base branch from master to main October 11, 2020 18:22
@tqchen
Copy link
Member

tqchen commented Oct 28, 2020

closing for now as per inactive status, feel free to reopen a new one

@tqchen tqchen closed this Oct 28, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants