diff --git a/.ci-check b/.ci-check new file mode 100644 index 00000000000..f896f5ccd9b --- /dev/null +++ b/.ci-check @@ -0,0 +1 @@ +CI check. No functional change; this branch is deleted after CI runs.