My holistic comprehension of launcher is weak, but I think that perhaps the cleanest thing would be to merge $user_args with $docker_args?
$user_argscomes from the command-line flag--docker-args, and$docker_argscomes from the config file yaml entry fordocker_args:.- The
$docker_argsvar is only used once in the entire launcher script (alongside$user_args, while$user_argsis used in all run invocations that I see.
Does merging $user_args and $docker_args into one $user_args var sound okay?
PS happy anniversary!