elsif (/--?platformfile=(.*)/) { $platformfile = $1; }
elsif (/--?hostfile=(.*)/) { $hostfile = $1; }
elsif (/--?srcdir=(.*)/) { $srcdir = $1;
elsif (/--?platformfile=(.*)/) { $platformfile = $1; }
elsif (/--?hostfile=(.*)/) { $hostfile = $1; }
elsif (/--?srcdir=(.*)/) { $srcdir = $1;