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.

Sign up for GitHub

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

Jump to bottom

./miri rustc-push suggests the flag --rustc-git but that flag isn't recognized #3173

Closed
saethlin opened this issue Nov 17, 2023 · 0 comments · Fixed by #3174
Closed

./miri rustc-push suggests the flag --rustc-git but that flag isn't recognized #3173

saethlin opened this issue Nov 17, 2023 · 0 comments · Fixed by #3174

Comments

@saethlin
Copy link
Member 

╭ ➜ ben@archlinux:~/miri
╰ ➤ ./miri rustc-push saethlin miri
This will pull a copy of the rust-lang/rust history into this Miri checkout, growing it by about 1GB.
To avoid that, abort now and set the `--rustc-git` flag to an existing rustc checkout. Proceed? [y/N] N
╭ ➜ ben@archlinux:~/miri
╰ ➤ ./miri rustc-push saethlin miri --rustc-git=/home/ben/rust
Error: Too many arguments for `./miri rustc-push GITHUB_USER BRANCH`
╭ ➜ ben@archlinux:~/miri
╰ ➤ ./miri --rustc-git=/home/ben/rust rustc-push saethlin miri
Unknown or missing command. Usage:
<snip>

This flag sounds useful, maybe we just need to fix some parsing?
@RalfJung RalfJung mentioned this issue Nov 18, 2023
Merged
@bors bors closed this as completed in 02baccc Nov 18, 2023
RalfJung pushed a commit to RalfJung/rust that referenced this issue Nov 25, 2023
@bors
Auto merge of rust-lang#3174 - RalfJung:rustc-git, r=RalfJung
b7b919c 
miri script: fix RUSTC_GIT error message

Making this a flag is tricky since our command-line parsing is pretty crude.

Fixes rust-lang/miri#3173
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

miri script: fix RUSTC_GIT error message RalfJung/miri
1 participant
@saethlin