diff --git a/tools/args b/tools/args index be8e7c9962b41c8ee3d65e4f6ad45f6ac84f47d6..bfd63f21deb2b4a85cc01774ae6a87359cf666bb 100755 Binary files a/tools/args and b/tools/args differ