github: Rename GitHub workflow action

GitHub checks need to be uniquely named, and 'Documentation' conflicts
with the ci-tool name.  Rename this while we are running both so the
names don't conflict.

Signed-off-by: Kumar Gala <kumar.gala@linaro.org>
This commit is contained in:
Kumar Gala 2020-02-08 07:41:47 -06:00 committed by Kumar Gala
commit b1de748948

View file

@ -1,7 +1,7 @@
# Copyright (c) 2020 Linaro Limited.
# SPDX-License-Identifier: Apache-2.0
name: Documentation
name: Documentation GitHub Workflow
on: [pull_request, push]