Merge pull request #1394 from bernt-matthias/topic/shed_lint_skip

add --skip to shed_lint
galaxyproject · Oct 18, 2023 · a6768bc · a6768bc
2 parents b7c79c5 + 7fcbdc3
commit a6768bc
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/planemo/commands/cmd_shed_lint.py b/planemo/commands/cmd_shed_lint.py
@@ -13,6 +13,7 @@
 @options.shed_realization_options()
 @options.report_level_option()
 @options.fail_level_option()
+@options.skip_option()
 @options.click.option(
     "--tools", is_flag=True, default=False, help=("Lint tools discovered in the process of linting repositories.")
 )