tree 57eda0d91fc1bfd9958830db6a0329cf82edb2d6
parent f17428a009c8fc544b6244bab951a153dff023eb
author Kumar Gala <kumar.gala@linaro.org> 1581169307 -0600
committer Kumar Gala <kumar.gala@gmail.com> 1581174350 -0600

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>