diff options
Diffstat (limited to 'tools/make-both-single-timing-files.py')
| -rwxr-xr-x | tools/make-both-single-timing-files.py | 18 |
1 files changed, 6 insertions, 12 deletions
diff --git a/tools/make-both-single-timing-files.py b/tools/make-both-single-timing-files.py index 2d33503c3..32c52c7a1 100755 --- a/tools/make-both-single-timing-files.py +++ b/tools/make-both-single-timing-files.py @@ -3,16 +3,10 @@ import sys from TimeFileMaker import * if __name__ == '__main__': - USAGE = 'Usage: %s AFTER_FILE_NAME BEFORE_FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0] + USAGE = 'Usage: %s [--sort-by=auto|absolute|diff] AFTER_FILE_NAME BEFORE_FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0] HELP_STRING = r'''Formats timing information from the output of two invocations of `coqc -time` into a sorted table''' - if len(sys.argv) < 3 or '--help' in sys.argv[1:] or '-h' in sys.argv[1:]: - print(USAGE) - if '--help' in sys.argv[1:] or '-h' in sys.argv[1:]: - print(HELP_STRING) - if len(sys.argv) == 2: sys.exit(0) - sys.exit(1) - else: - left_dict = get_single_file_times(sys.argv[1]) - right_dict = get_single_file_times(sys.argv[2]) - table = make_diff_table_string(left_dict, right_dict, tag="Code") - print_or_write_table(table, sys.argv[3:]) + sort_by, args = parse_args(sys.argv, USAGE, HELP_STRING) + left_dict = get_single_file_times(args[1]) + right_dict = get_single_file_times(args[2]) + table = make_diff_table_string(left_dict, right_dict, tag="Code", sort_by=sort_by) + print_or_write_table(table, args[3:]) |