aboutsummaryrefslogtreecommitdiff
path: root/dev/include_printers
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-09-18 14:41:05 +0000
committerGitHub2020-09-18 14:41:05 +0000
commit5bdd954f57aa9e7154258f38619c6be7b6ba2d7c (patch)
treefe6aba4f5ee1b955360836357e1b980e6a51c670 /dev/include_printers
parentff508baf8de691dfa94b9d65d7c77cf395127381 (diff)
parent37b16d6ad093ae958c942a94b6070bc72b744f77 (diff)
Merge PR #13043: [ci] call dmesg after quick/async jobs to detect OOM
Reviewed-by: Zimmi48
Diffstat (limited to 'dev/include_printers')
0 files changed, 0 insertions, 0 deletions