diff options
| author | Rémi Verschelde <remi@verschelde.fr> | 2022-06-15 23:33:15 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-06-15 23:33:15 +0200 |
| commit | 2f9b7b7a605f20321c1a239935152723bc13edf0 (patch) | |
| tree | 5e8c6e305b9512ad99b019507fa03f32002d3efa /misc/scripts | |
| parent | 421d8b716db25a7556d428b7bb210ce4d94caa0b (diff) | |
| parent | 80237a54e01dd964cc4242ebc5979087a3b67d68 (diff) | |
Merge pull request #62082 from qarmin/handle_crash_ci
Stop CI when Godot crash
Diffstat (limited to 'misc/scripts')
| -rwxr-xr-x | misc/scripts/check_ci_log.py | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/misc/scripts/check_ci_log.py b/misc/scripts/check_ci_log.py index 2c75b83bd7..1e5a12eeb4 100755 --- a/misc/scripts/check_ci_log.py +++ b/misc/scripts/check_ci_log.py @@ -25,6 +25,8 @@ if ( file_contents.find("Program crashed with signal") != -1 or file_contents.find("Dumping the backtrace") != -1 or file_contents.find("Segmentation fault (core dumped)") != -1 + or file_contents.find("Aborted (core dumped)") != -1 + or file_contents.find("terminate called without an active exception") != -1 ): print("FATAL ERROR: Godot has been crashed.") sys.exit(52) |