use OPTION_ERROR as exit code for wrong PR number

lexming · boegel · web-flow · commit 79e019b7c243 · 2024-09-17T14:09:30.000+02:00
Co-authored-by: Kenneth Hoste &lt;kenneth.hoste@ugent.be&gt;
diff --git a/easybuild/tools/github.py b/easybuild/tools/github.py
@@ -829,7 +829,7 @@ def post_comment_in_issue(issue, txt, account=GITHUB_EB_MAIN, repo=GITHUB_EASYCO
         except ValueError as err:
             raise EasyBuildError(
                 "Failed to parse specified pull request number '%s' as an int: %s; ", issue, err,
-                exit_code=EasyBuildExit.FAIL_GITHUB
+                exit_code=EasyBuildExit.OPTION_ERROR
             )
 
     dry_run = build_option('dry_run') or build_option('extended_dry_run')

Original file line number	Diff line number	Diff line change
`@@ -829,7 +829,7 @@ def post_comment_in_issue(issue, txt, account=GITHUB_EB_MAIN, repo=GITHUB_EASYCO`
`829`	`829`	`except ValueError as err:`
`830`	`830`	`raise EasyBuildError(`
`831`	`831`	`"Failed to parse specified pull request number '%s' as an int: %s; ", issue, err,`
`832`		`- exit_code=EasyBuildExit.FAIL_GITHUB`
	`832`	`+ exit_code=EasyBuildExit.OPTION_ERROR`
`833`	`833`	`)`
`834`	`834`
`835`	`835`	`dry_run = build_option('dry_run') or build_option('extended_dry_run')`