aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEelco Dolstra <e.dolstra@tudelft.nl>2003-11-03 18:21:53 +0000
committerEelco Dolstra <e.dolstra@tudelft.nl>2003-11-03 18:21:53 +0000
commitff3132427839888933c3779844bf35ca9e189cb9 (patch)
treea971b049852cba9730683f89de5d8e41804f2f62
parente2655aa332a33b56d9168928511a598fc9b0c1e6 (diff)
* Ignore options passed to the aterm library.
-rw-r--r--src/libmain/shared.cc7
1 files changed, 5 insertions, 2 deletions
diff --git a/src/libmain/shared.cc b/src/libmain/shared.cc
index 80463308a..39439f8e1 100644
--- a/src/libmain/shared.cc
+++ b/src/libmain/shared.cc
@@ -26,12 +26,15 @@ static void initAndRun(int argc, char * * argv)
while (argc--) args.push_back(*argv++);
args.erase(args.begin());
- /* Expand compound dash options (i.e., `-qlf' -> `-q -l -f'). */
+ /* Expand compound dash options (i.e., `-qlf' -> `-q -l -f'), and
+ ignore options for the ATerm library. */
for (Strings::iterator it = args.begin();
it != args.end(); )
{
string arg = *it;
- if (arg.length() > 2 && arg[0] == '-' && arg[1] != '-') {
+ if (string(arg, 0, 4) == "-at-")
+ it = args.erase(it);
+ else if (arg.length() > 2 && arg[0] == '-' && arg[1] != '-') {
for (unsigned int i = 1; i < arg.length(); i++)
if (isalpha(arg[i]))
args.insert(it, (string) "-" + arg[i]);