aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-12-02 13:01:34 +0000
committerGitHub2020-12-02 13:01:34 +0000
commitad8cf0108e628710128e5a6e266b72895eed98b9 (patch)
treebd95e4a97b27a56845b5a5401e08cd8c1759a82f /kernel
parentff8155bf6586040b92d916a72017ac1bdc138501 (diff)
parent61a784aa031d1fcb0913e83206faa5265e3f5a17 (diff)
Merge PR #13471: gitlab CI: remove redundant "dependencies" info
Reviewed-by: Zimmi48
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions