name change for args

2019-04-25 08:57:56 -07:00 · 2019-04-25 08:57:56 -07:00 · b369913249
commit b369913249
parent 596199aa8b
1 changed files with 1 additions and 1 deletions
--- a/bin/deepstate/eclipser.py
+++ b/bin/deepstate/eclipser.py
@ -68,7 +68,7 @@ def main():
  if args.which_test is not None:
      deepargs += " --input_which_test " + args.which_test
  cmd += ["--initarg", deepargs, "--maxfilelen", str(args.max_input_size)]
-  cmd += args.eclipserargs
+  cmd += args.args
  try:
    r = subprocess.call(cmd)
    print ("Eclipser finished with exit code", r)