diff options
Diffstat (limited to 'src/micro/port_linux.c')
| -rw-r--r-- | src/micro/port_linux.c | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/micro/port_linux.c b/src/micro/port_linux.c index 9331a0b..6245f4f 100644 --- a/src/micro/port_linux.c +++ b/src/micro/port_linux.c @@ -372,7 +372,7 @@ int main(int argc, char **argv) { " TINYVM_MAX_MEMORY_WORDS maximum vm memory in words\n", stdout); return 0; } - if (argc > 1 && argv[1][0] == '-' && argv[1][1] == '-') { + if (argc > 1 && argv[1][0] == '-' && argv[1][1] == '-' && strcmp(argv[1], "--explain-checks")) { /* the compiler reads that one */ fprintf(stderr, "micro: unknown option %s; use --help for usage\n", argv[1]); return 2; } |