Uh oh!
There was an error while loading. Please reload this page.
Allow use of docker/lint.sh clang_format with git-worktree - #8639
Allow use of docker/lint.sh clang_format with git-worktree#8639areusch wants to merge 2 commits into
Conversation
tqchen
commented
Aug 3, 2021
@areusch let us do a quick check in case some of the CI might depend on the /workspace behavior |
areusch
commented
Aug 3, 2021
@tqchen last time it was the rust rebuild which is conveniently disabled now :) |
areusch
commented
Aug 3, 2021
not that i am trying to actively break rust but i don't understand the build system enough to know how to fix it and last time the PR languished forever and died because no one was willing to help. |
* properly quote command-line arguments * mount repo at $(pwd) by default; fixes problems when using git-worktree.
9050f57 to
339ebdaCompare
leandron
left a comment
There was a problem hiding this comment.
* mount repo at $(pwd) by default; fixes problems when using git-worktree.
What is the problem when using git-worktree? I'm not very familiar with it.
* allows usage of docker/lint.sh with arbitrary tvm repo
Maybe we could add a "usage" example in the header of the script, to instruct people on how to do that?
Also, a bit off topic for here but I think we really should think about processing the inputs in a loop so that users can provide non-positional parameters in any order.
| SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" | ||
| WORKSPACE="$(pwd)" | ||
| if [ "$1" == "--repo-mount-point" ]; then |
There was a problem hiding this comment.
It would be good to add this on line 23 small documentation to the command line, also to show the order in which parameters need to be provided.
areusch
commented
Aug 4, 2021
@leandron try running
ack
will see if i can do this in next patch |
areusch
commented
Aug 10, 2021
superseded by #8670 |
cc @jroesch@mikepapadim@tqchen