use FAIL_GITHUB exit code for failure to fetch files of easyconfig PR

lexming · boegel · web-flow · commit 8f4304f7fde1 · 2024-09-17T14:05:39.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
@@ -504,7 +504,7 @@ def fetch_files_from_pr(pr, path=None, github_user=None, github_account=None, gi
                 else:
                     raise EasyBuildError(
                         "Failed to isolate path for PR #%s from list of PR paths: %s", pr, extra_ec_paths,
-                        exit_code=EasyBuildExit.OPTION_ERROR
+                        exit_code=EasyBuildExit.FAIL_GITHUB
                     )
 
         elif github_repo == GITHUB_EASYBLOCKS_REPO:

Original file line number	Diff line number	Diff line change
`@@ -504,7 +504,7 @@ def fetch_files_from_pr(pr, path=None, github_user=None, github_account=None, gi`
`504`	`504`	`else:`
`505`	`505`	`raise EasyBuildError(`
`506`	`506`	`"Failed to isolate path for PR #%s from list of PR paths: %s", pr, extra_ec_paths,`
`507`		`- exit_code=EasyBuildExit.OPTION_ERROR`
	`507`	`+ exit_code=EasyBuildExit.FAIL_GITHUB`
`508`	`508`	`)`
`509`	`509`
`510`	`510`	`elif github_repo == GITHUB_EASYBLOCKS_REPO:`