diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/libmain/shared.cc | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/libmain/shared.cc b/src/libmain/shared.cc index a390654452ed..14263446fe2e 100644 --- a/src/libmain/shared.cc +++ b/src/libmain/shared.cc @@ -220,6 +220,13 @@ static void initAndRun(int argc, char * * argv) string value = *i; settings.set(name, value); } + else if (arg == "--arg" || arg == "--argstr") { + remaining.push_back(arg); + ++i; if (i == args.end()) throw UsageError(format("`%1%' requires two arguments") % arg); + remaining.push_back(*i); + ++i; if (i == args.end()) throw UsageError(format("`%1%' requires two arguments") % arg); + remaining.push_back(*i); + } else remaining.push_back(arg); } |