about summary refs log tree commit diff
diff options
context:
space:
mode:
authorRalf Jung <post@ralfj.de>2024-12-28 08:17:04 +0000
committerGitHub <noreply@github.com>2024-12-28 08:17:04 +0000
commit3fceb037d53c93b443ece98935f7db73f34dc9fa (patch)
tree9bd5d9387b483e1b6d3ab7a493486ad331d3e685
parent5ccf10edf133ad673429ab4e7090459689c78b57 (diff)
parent0eb5acea2dc3706faa3d84d3c0ad20bd546b3118 (diff)
downloadrust-3fceb037d53c93b443ece98935f7db73f34dc9fa.tar.gz
rust-3fceb037d53c93b443ece98935f7db73f34dc9fa.zip
Merge pull request #4113 from rmehri01/toolchain-parsing
fix toolchain flag parsing
-rw-r--r--src/tools/miri/miri-script/src/main.rs1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/tools/miri/miri-script/src/main.rs b/src/tools/miri/miri-script/src/main.rs
index a80fed8fcb6..279bdf8cc3f 100644
--- a/src/tools/miri/miri-script/src/main.rs
+++ b/src/tools/miri/miri-script/src/main.rs
@@ -111,6 +111,7 @@ pub enum Command {
     /// `rustup-toolchain-install-master` must be installed for this to work.
     Toolchain {
         /// Flags that are passed through to `rustup-toolchain-install-master`.
+        #[arg(trailing_var_arg = true, allow_hyphen_values = true)]
         flags: Vec<String>,
     },
     /// Pull and merge Miri changes from the rustc repo.