alaviss 40898871a9 workflows/ci_docs: fix documentation deployment (#13819) ...

* workflows/ci_docs: fix docs publishing

It turns out that github.ref is the full ref name, so we have to be a
bit more specific.

See https://developer.github.com/v3/activity/events/types/#pushevent

Also fixed a silly typo :)

* workflows/ci_docs: run CI when there are changes to the workflow

2020-03-31 19:36:37 +02:00

..

ci_docs.yml

workflows/ci_docs: fix documentation deployment (#13819)

2020-03-31 19:36:37 +02:00

ci_ssl.yml

SSL certificate verify GitHub action (#13697)

2020-03-20 17:11:39 +01:00

ci.yml.disabled

workflows/ci: disable

2020-03-17 08:48:42 +01:00