Skip to content

Commit b71a830

Browse files
author
martin
committed
Remove the --mm option from goto-diff
This was tested for but does not appear as an option in goto_diff_parse_options.h as a valid option so this code can never be used. Worse, goto-diff doesn't include any of the code that uses it, nor can I think what the memory model might have to do with diffing goto-programs.
1 parent b1c61dc commit b71a830

File tree

1 file changed

+0
-3
lines changed

1 file changed

+0
-3
lines changed

src/goto-diff/goto_diff_parse_options.cpp

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -70,9 +70,6 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options)
7070
if(cmdline.isset("cover"))
7171
parse_cover_options(cmdline, options);
7272

73-
if(cmdline.isset("mm"))
74-
options.set_option("mm", cmdline.get_value("mm"));
75-
7673
// all checks supported by goto_check
7774
PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
7875

0 commit comments

Comments
 (0)